HowToUseC API

This page shows an example of how to use C++ API. Consider we want to perform static analysis on the following C-like program:

  int i,x,y;
  i=0;
  x=1;
  y=0;
  while (i < 100) {
	x=x+y;
	y=y+1;
	i=i+1;
  }	 

This is the (simplified) C++ code to build the corresponding CrabIR program and run the analysis using the Zones domain.

Note: the code has been simplified for presentation purposes and it might not compile like it is. Take a look at this for a real example.

    // CFG-based language
    #include<crab/cfg/cfg.hpp>
    // Variable factory	
    #include<crab/types/varname_factory.hpp>
    #include<crab/types/variable.hpp> 
    // Intra forward analyzer	
    #include<crab/analysis/fwd_analyzer.hpp>
    // Zones domain
    #include<crab/domains/split_dbm.hpp>
    /* 
      To define a Control-Flow Graph (CFG) users need to define :
      (1) Type for a variable name
      (2) Type for a basic block label
      (3) Choose between integers or rationals (Crab cannot mix them)
    */
    // (1) A variable factory based on strings
    using variable_factory_t = crab::var_factory_impl::str_variable_factory;
    using varname_t = typename variable_factory_t::varname_t;
    // (2) CFG basic block labels
    using basic_block_label_t = std::string;
    // (3) CFG over integers
	using z_cfg_t = crab::cfg::cfg<basic_block_label_t, varname_t, z_number>;
    using z_cfg_ref_t = crab::cfg::cfg_ref<z_cfg_t>;

    // Abstract domain: zones domain
    using zones_domain_t = domains::split_dbm_domain<z_number, varname_t>;
    // Generic domain that hides the actual domain: type-erasure pattern in C++
    using abs_domain_t = domains::abstract_domain<var_t>;
    // Intra-procedural analysis 
    using fwd_analyzer_t = analyzer::intra_fwd_analyzer<cfg_ref_t, abs_domain_t>;

    int main (int argc, char**argv) {
       // Create variable factory. 
       // Important: only one variable factory should be used to build a CFG. 
       // Moreover, the variable factory should be alive while the CFG is in use.
       variable_factory_t vfac;	
       // Declare variables i,x, and y
       z_var i(vfac["i"], INT_TYPE, 32);
       z_var x(vfac["x"], INT_TYPE, 32);
       z_var y(vfac["y"], INT_TYPE, 32);
	   
       // Create an empty CFG marking "entry" and "exit" are the labels
       // for the entry and exit blocks.
       cfg_t cfg("entry","ret");
	   
       // Add blocks
       basic_block_t& entry = cfg.insert("entry");
       basic_block_t& bb1   = cfg.insert("bb1");
       basic_block_t& bb1_t = cfg.insert("bb1_t");
       basic_block_t& bb1_f = cfg.insert("bb1_f");
       basic_block_t& bb2   = cfg.insert("bb2");
       basic_block_t& ret   = cfg.insert("ret");
	   
       // Add control flow 
       entry.add_succ(bb1); bb1.add_succ(bb1_t); bb1.add_succ(bb1_f);
       bb1_t.add_succ(bb2); bb2.add_succ(bb1); bb1_f.add_succ(ret);
	   
       // Add statements
       entry.assign(i, 0);
       entry.assign(x, 1);
       entry.assign(y, 0);
       bb1_t.assume(i <= 99);
       bb1_f.assume(i >= 100);
       bb2.add(x,x,y);
       bb2.add(y,y,1);
       bb2.add(i,i,1);

       // Build an analyzer and run the zones domain
       zones_domain_t top_zones;  // initially top
       abs_domain_t init(top_zones);
       fwd_analyzer_t analyzer(cfg, init);
       a.run();
	   	
       // Scan all CFG basic blocks and print the invariants that hold
       // at their entries
       cout << "Invariants using zones:\n";	   
       for (auto &b : cfg) {
           auto bb_name = bb.label();
           auto inv = analyzer.get_pre(bb_name);
           crab::outs () << bb_name << ":" << inv << "\n";
       }
       return 0;
    }

The Crab output of this program, showing the invariants that hold at the entry of each basic block, should be something like this:

Invariants using zones:

entry={}
bb1={i -> [0, 100], x -> [1, +oo], y -> [0, 100], y-i<=0, y-x<=0, i-x<=0, i-y<=0}
bb1_t={i -> [0, 100], x -> [1, +oo], y -> [0, 100], y-i<=0, y-x<=0, i-x<=0, i-y<=0}
bb1_f={i -> [0, 100], x -> [1, +oo], y -> [0, 100], y-i<=0, y-x<=0, i-x<=0, i-y<=0}
bb2={i -> [0, 99], x -> [1, +oo], y -> [0, 99], y-i<=0, y-x<=0, i-x<=0, i-y<=0}
ret={i -> [100, 100], x -> [100, +oo], y -> [100, 100], y-i<=0, y-x<=0, i-x<=0, i-y<=0}