ClamAPIUsage

This is a complete C++ program that reads a LLVM bitcode file and runs the Clam analysis on it to print invariants and prove assertions (if any).

// LLVM header files
#include "llvm/Analysis/CallGraph.h"
#include "llvm/Analysis/TargetLibraryInfo.h"
#include "llvm/Bitcode/BitcodeWriter.h"
#include "llvm/IR/LLVMContext.h"
#include "llvm/IR/Module.h"
#include "llvm/IR/PassManager.h"
#include "llvm/IRReader/IRReader.h"
#include "llvm/IR/Function.h"
#include "llvm/Support/SourceMgr.h"

// SeaDsa header files
#include "seadsa/AllocWrapInfo.hh"
#include "seadsa/DsaLibFuncInfo.hh"

// Clam header files
#include "clam/Clam.hh"
#include "clam/CfgBuilder.hh"
#include "clam/HeapAbstraction.hh"
#include "clam/SeaDsaHeapAbstraction.hh"

using namespace clam;
using namespace llvm;

int main(int argc, char *argv[]) {
  if (argc < 2) {
    llvm::errs() << "Not found input file\n";
    llvm::errs() << "Usage " << argv[0] << " " << "FILE.bc\n";
    return 1;
  }
  
  //////////////////////////////////////  
  // Get module from LLVM file
  //////////////////////////////////////  
  LLVMContext Context;
  SMDiagnostic Err;
  std::unique_ptr<Module> module = parseIRFile(argv[1], Err, Context);
  if (!module) {
    Err.print(argv[0], errs());
    return 1;
  }
  
  const auto& tripleS = module->getTargetTriple();
  Twine tripleT(tripleS);
  Triple triple(tripleT);
  TargetLibraryInfoWrapperPass  TLIW(triple);  

  //////////////////////////////////////
  // Run seadsa -- pointer analysis
  //////////////////////////////////////  
  CallGraph cg(*module);
  seadsa::AllocWrapInfo allocWrapInfo(&TLIW);
  allocWrapInfo.initialize(*module, nullptr);
  seadsa::DsaLibFuncInfo dsaLibFuncInfo;
  dsaLibFuncInfo.initialize(*module);
  std::unique_ptr<HeapAbstraction> mem(new SeaDsaHeapAbstraction(
		*module, cg, TLIW, allocWrapInfo, dsaLibFuncInfo, true));

  //////////////////////////////////////  
  // Clam
  //////////////////////////////////////
  
  /// Translation from LLVM to CrabIR
  CrabBuilderParams cparams;
  cparams.setPrecision(clam::CrabBuilderPrecision::MEM);
  cparams.print_cfg = true;
  CrabBuilderManager man(cparams, TLIW, std::move(mem));
  
  /// Set Crab parameters
  AnalysisParams aparams;
  aparams.dom = CrabDomain::INTERVALS;
  aparams.run_inter = true;
  aparams.check = clam::CheckerKind::ASSERTION;
  
  /// Create an inter-analysis instance 
  InterGlobalClam ga(*module, man);
  /// Run the Crab analysis
  ClamGlobalAnalysis::abs_dom_map_t assumptions;
  ga.analyze(aparams, assumptions);
  
  /// Print program invariants inferred by Clam
  llvm::errs() << "===Invariants at the entry of each block===\n";
  for (auto &f: *module) {
    for (auto &b: f) {
      llvm::Optional<clam_abstract_domain> dom = ga.getPre(&b);
      if (dom.hasValue()) {
	crab::outs() << f.getName() << "#" << b.getName() << ":\n  " << dom.getValue() << "\n";
      }
    }
  }
  llvm::errs() << "===Ranges for each Instruction's definition===\n";
  for (auto &f: *module) {
    for (auto &b: f) {
      for (auto &i: b) {
	if (!i.getType()->isVoidTy()) {
	  auto rangeVal = ga.range(i);
	  llvm::errs() << "Range for " << i << " = " << rangeVal << "\n";
	}
      }
    }
  }
  
  /// Print results about assertion checks
  llvm::errs() << "===Assertion checks ===\n";
  ga.getChecksDB().write(crab::outs());
  
  return 0;
}

This is the Makefile to compile the above program:

# Installation directory for clam
CLAM_INSTALL=${HOME}/Repos/clam-dev10/install-release
# Installation directory for llvm
LLVM_HOME=${HOME}/src/clang+llvm-10.0.0-x86_64-apple-darwin

ifeq ($(LLVM_CONFIG),)
	LLVM_CONFIG=llvm-config
endif

LLVM_CFG = $(LLVM_HOME)/bin/$(LLVM_CONFIG)

CLAM_INCLUDE := \
	-I/usr/local/include \
	-I${CLAM_INSTALL}/crab/include \
	-I${CLAM_INSTALL}/ldd/include \
	-I${CLAM_INSTALL}/elina/include \
	-I${CLAM_INSTALL}/apron/include \
	-I${CLAM_INSTALL}/include

#LLVM_INCLUDE := $(shell ${LLVM_CFG} --includedir)

CXXFLAGS := \
	$(shell  ${LLVM_CFG} --cxxflags) \
	-fPIC -std=c++14 \
	-fvisibility-inlines-hidden -Werror=date-time -Wno-unused-local-typedef \
	-Wno-redeclared-class-member -Wno-sometimes-uninitialized \
	-Wno-deprecated-declarations -fcxx-exceptions -Wno-covered-switch-default \
	-Wno-inconsistent-missing-override \
	-D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS \
	-g -O2 -DNDEBUG \
	$(CLAM_INCLUDE) \
	$(LLVM_INCLUDE)

LLVM_LIBS := $(shell ${LLVM_CFG} --libs)

CRAB_LIBS := ${CLAM_INSTALL}/crab/lib/libCrab.a


CLAM_LIBS := \
	$(CLAM_INSTALL)/lib/libClamAnalysis.a \
	$(CLAM_INSTALL)/lib/libSeaDsaAnalysis.a 
CLAM_LIBS += ${CRAB_LIBS}

# to use APRON, pass MOD=APRON in make invocation
MOD ?= APRON
ifeq ($(MOD),ELINA)
    MOD := ELINA
    mod := elina
else
    MOD := APRON
    mod := apron
endif

MODINSTALL := ${CLAM_INSTALL}/$(mod)

ifeq ($(MOD),ELINA)
    CLAM_LIBS += \
        $(MODINSTALL)/lib/libelinalinearize.so \
        $(MODINSTALL)/lib/libelinaux.so \
        $(MODINSTALL)/lib/liboptoct.so \
        $(MODINSTALL)/lib/liboptpoly.so \
        $(MODINSTALL)/lib/liboptzones.so \
        $(MODINSTALL)/lib/libpartitions.so
else
    CLAM_LIBS += \
        $(MODINSTALL)/lib/libpolkaMPQ.a \
        $(MODINSTALL)/lib/liboctD.a \
        $(MODINSTALL)/lib/liboptoct.a \
        $(MODINSTALL)/lib/liblinkedlistapi.a \
        $(MODINSTALL)/lib/libapron.a \
        $(MODINSTALL)/lib/libboxMPQ.a \
        $(MODINSTALL)/lib/libitvMPQ.a
endif

LDDINSTALL=$(CLAM_INSTALL)/ldd

CLAM_LIBS += \
    $(LDDINSTALL)/lib/libtvpi.a \
    $(LDDINSTALL)/lib/libcudd.a \
    $(LDDINSTALL)/lib/libst.a \
    $(LDDINSTALL)/lib/libutil.a \
    $(LDDINSTALL)/lib/libmtr.a \
    $(LDDINSTALL)/lib/libepd.a \
    $(LDDINSTALL)/lib/libldd.a \


LDLIBS := \
     $(CLAM_LIBS) $(LLVM_LIBS) \
     -lmpfr -lgmpxx -lgmp -lm -lncurses

LLVM_LDFLAGS= $(shell ${LLVM_CFG} --ldflags)
LDFLAGS := $(LLVM_LDFLAGS)

TOOL=myanalyzer

all: $(TOOL)

%.o:  $(CXX) $(CXXFLAGS) $< -c -o $@

$(TOOL): $(TOOL).o
	$(CXX) $(LDFLAGS) $(TOOL).o $(LDLIBS) -o $(TOOL)

clean:
	rm -f $(TOOL).o $(TOOL)