Merge pull request diffblue#19 from lefanz-amazon/lefan-abstraction

length: add length variable and assumptions

Author: Lefan Zhang

regression/abstraction/abst-funcs.c

@@ -118,7 +118,7 @@ size_t sub_conc_from_abs_1(size_t abs_ind, size_t num, size_t a1){
 //Cases +c+c*, c+c*, +cc*, c+c*, cc+ can all be 
 //handled by the same function as long as we are careful with concretization, increment and other funcs.
 //If model checking time is affected then we can split into finer cases.
-int two_abs(int index, int a1, int a2) {
+size_t two_abs(size_t index, size_t a1, size_t a2) {
     if (index < a1) return 0;
     else if (index == a1) return 1;
     else if (index > a1 && index < a2) return 2;
@@ -129,7 +129,7 @@ int two_abs(int index, int a1, int a2) {
 
 //Get the concretization of an index. We assume all args are >= 0
 //Shape *c*c*
-int concretize_2(int abs_ind, int a1, int a2) {
+size_t concretize_2(size_t abs_ind, size_t a1, size_t a2) {
     assert(abs_ind >= 0);
     assert(a1 >= 0);
     assert(a2 > a1);
@@ -155,18 +155,18 @@ int concretize_2(int abs_ind, int a1, int a2) {
     else return(nndt_above(a2));
 }
 
-int is_precise_2(int abs_ind){
+int is_precise_2(size_t abs_ind){
     if (abs_ind == 1 || abs_ind == 3) return(1);
     else return(0);
 }
 
-int is_abstract_2(int abs_ind){
+int is_abstract_2(size_t abs_ind){
     int pre = is_precise_2(abs_ind);
     return(1-pre);
 }
 
 // Add a number to an abs_ind
-int add_abs_to_conc_2(int abs_ind, int num, int a1, int a2){
+size_t add_abs_to_conc_2(size_t abs_ind, size_t num, size_t a1, size_t a2){
     if (num == 1){
         if(abs_ind == 0 || abs_ind == 2) {
             if (nndt_bool() > 0) return(abs_ind);
@@ -190,7 +190,7 @@ int add_abs_to_conc_2(int abs_ind, int num, int a1, int a2){
 
 }
 
-int sub_conc_from_abs_2(int abs_ind, int num, int a1, int a2){
+size_t sub_conc_from_abs_2(size_t abs_ind, size_t num, size_t a1, size_t a2){
     if (num == 1){
         if(abs_ind == 4 || abs_ind == 2) {
             if (nndt_bool() > 0) return(abs_ind);

regression/abstraction/specs/aws_array_eq.json

@@ -5,17 +5,17 @@
             "function": "aws_array_eq_harness",
             "name": "aws_array_eq_harness::1::rhs",
             "shape": {
-                "indices": ["cncrt"],
+                "indices": ["cncrt", "length"],
                 "assumptions": [
                 ],
-                "shape-type": "*c*"
+                "shape-type": "*c*l"
             },
-            "abst-function-file": "./abst-funcs.c",
+            "abst-function-file": "../abst-funcs.c",
             "abst-functions":{
-                "add-abs-conc": "add_abs_to_conc_1",
-                "sub-abs-conc": "sub_conc_from_abs_1",
-                "precise-check": "is_precise_1",
-                "abstract-index": "one_abs",
+                "add-abs-conc": "add_abs_to_conc_2",
+                "sub-abs-conc": "sub_conc_from_abs_2",
+                "precise-check": "is_precise_2",
+                "abstract-index": "two_abs",
                 "concretize-index": "concretize",
                 "multiply-indices": null,
                 "mod-indices": null
@@ -27,12 +27,7 @@
                     "name": "aws_array_eq_harness::1::lhs"
                 },
                 {
-                    "entity": "scalar",
-                    "function": "aws_array_eq_harness",
-                    "name": "aws_array_eq_harness::1::rhs_len"
-                },
-                {
-                    "entity": "scalar",
+                    "entity": "length",
                     "function": "aws_array_eq_harness",
                     "name": "aws_array_eq_harness::1::lhs_len"
                 }

src/goto-instrument/abstraction.cpp

@@ -294,10 +294,10 @@ void complete_abst_spec(const goto_functiont& goto_function, abstraction_spect &
       std::tuple<std::unordered_set<irep_idt>, std::unordered_set<irep_idt>> abst_entities = find_index_symbols(goto_function, ent.first);
       for(irep_idt index_name: std::get<0>(abst_entities))
         if(spec.get_abst_arrays().find(index_name) == spec.get_abst_arrays().end())
-          spec.insert_entity(index_name, false);
+          spec.insert_entity(index_name, "array");
       for(irep_idt index_name: std::get<1>(abst_entities))
         if(spec.get_abst_indices().find(index_name) == spec.get_abst_indices().end())
-          spec.insert_entity(index_name, true);
+          spec.insert_entity(index_name, "scalar");
     }
   }
 }
@@ -1235,11 +1235,102 @@ void define_concrete_indices(goto_modelt &goto_model, const abstraction_spect &a
   }
 }
 
+void add_length_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec)
+{
+  for(const auto &spec: abst_spec.get_specs())
+  {
+    for(const auto &lp: spec.get_abst_lengths())
+    {
+      const irep_idt func_name = abst_spec.get_func_name();
+
+      // TODO: currently we are assuming every entities in the 
+      // json file belong to the same function. That may not be the case.
+      auto &function = goto_model.goto_functions.function_map.at(func_name);
+      // if this variable is a local varible
+      bool is_local = false;
+
+      // go through each instruction in the function to find the declare
+      Forall_goto_program_instructions(it, function.body)
+      {
+        if(it->is_decl())
+        {
+          const code_declt &decl = it->get_decl();
+          // check if this declares the length variable
+          if(decl.get_identifier() == lp.first)
+          {
+            is_local = true;
+            // need to add an assumption after this inst
+            INVARIANT(
+              goto_model.get_symbol_table().has_symbol(decl.get_identifier()),
+              "Symbol " + std::string(decl.get_identifier().c_str()) +
+                " not defined");
+            INVARIANT(
+              goto_model.get_symbol_table().has_symbol(
+                spec.get_length_index_name()),
+              "Symbol " + std::string(spec.get_length_index_name().c_str()) +
+                " not defined");
+
+            // define the assumption instruction
+            const symbolt symb1 = goto_model.get_symbol_table().lookup_ref(decl.get_identifier());
+            const symbolt symb2 = goto_model.get_symbol_table().lookup_ref(spec.get_length_index_name());
+            equal_exprt assumption_expr(symb1.symbol_expr(), symb2.symbol_expr());
+            auto new_assumption = goto_programt::make_assumption(assumption_expr);
+
+            // insert it
+            function.body.insert_after(it, new_assumption);
+            std::cout << "Added length assumption after the decl: ";
+            format_rec(std::cout, assumption_expr) << std::endl;
+            it++;
+          }
+        }
+      }
+
+      // if it is not a local variable, the assumption should be added at 
+      // the end of the global INITIAL function
+      if(!is_local)
+      {
+        // find the CPROVER_INITIAL function
+        goto_functionst::function_mapt::iterator fct_entry =
+          goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION);
+        CHECK_RETURN(fct_entry != goto_model.goto_functions.function_map.end());
+        goto_programt &init_function = fct_entry->second.body;
+        auto last_instruction = std::prev(init_function.instructions.end());
+        DATA_INVARIANT(
+          last_instruction->is_end_function(),
+          "last instruction in function should be END_FUNCTION");
+        
+        // define the assumption instruction
+        INVARIANT(
+          goto_model.get_symbol_table().has_symbol(lp.first),
+          "Symbol " + std::string(lp.first.c_str()) +
+            " not defined");
+        INVARIANT(
+          goto_model.get_symbol_table().has_symbol(
+            spec.get_length_index_name()),
+          "Symbol " + std::string(spec.get_length_index_name().c_str()) +
+            " not defined");
+        const symbolt symb1 = goto_model.get_symbol_table().lookup_ref(lp.first);
+        const symbolt symb2 = goto_model.get_symbol_table().lookup_ref(spec.get_length_index_name());
+        equal_exprt assumption_expr(symb1.symbol_expr(), symb2.symbol_expr());
+        auto new_assumption = goto_programt::make_assumption(assumption_expr);
+
+        // insert it
+        std::cout << "Added length assumption in the beginning of the function: ";
+        format_rec(std::cout, assumption_expr);
+        init_function.insert_before_swap(last_instruction, new_assumption);
+      }
+    }
+  }
+}
+
 void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec)
 {
   // Define the global concrete indices to be used
   define_concrete_indices(goto_model, abst_spec);
 
+  // Add the assumption for len==$clen
+  add_length_assumptions(goto_model, abst_spec);
+
   // A couple of spects are initialized from the json file. We should go from there and insert spects to other functions
   std::unordered_map<irep_idt, abstraction_spect> function_spec_map =
     calculate_complete_abst_specs_for_funcs(goto_model, abst_spec);

src/goto-instrument/abstraction.h

@@ -239,6 +239,9 @@ exprt abstract_expr_read(
   goto_programt::instructionst &insts_after,
   std::vector<symbolt> &new_symbs);
 
+// add the assumption len=$clen for all length variables
+void add_length_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec);
+
 // define concrete indices globally
 void define_concrete_indices(goto_modelt &goto_model, const abstraction_spect &abst_spec);
 

src/goto-instrument/abstraction_spect.cpp

@@ -30,12 +30,12 @@ abstraction_spect::abstraction_spect(
     size_t spec_index = specs.size();
     function = entry_obj.find("function")->second.value;  // we assume that all entries in the json file are located in the same function
     // insert the entity
-    spec.insert_entity(entry_obj.find("name")->second.value, entry_obj.find("entity")->second.value!="array");
+    spec.insert_entity(entry_obj.find("name")->second.value, entry_obj.find("entity")->second.value);
     const auto &json_re_array = to_json_array(entry_obj.find("related-entities")->second);
     for(auto it_r=json_re_array.begin(); it_r != json_re_array.end(); ++it_r)
     {
       const auto &related_entity = to_json_object(*it_r);
-      spec.insert_entity(related_entity.find("name")->second.value, related_entity.find("entity")->second.value!="array");
+      spec.insert_entity(related_entity.find("name")->second.value, related_entity.find("entity")->second.value);
     }
 
     // initialize the abst functions

src/goto-instrument/abstraction_spect.h

@@ -85,6 +85,11 @@ class abstraction_spect
       {
         return indices;
       }
+      const irep_idt get_length_index_name() const
+      {
+        INVARIANT(indices.size()>0, "shape should have at least a length concrete variable");
+        return *(indices.end()-1);
+      }
     };
 
     struct entityt
@@ -126,11 +131,12 @@ class abstraction_spect
 
     //Arrays to be abstracted
     std::unordered_map<irep_idt, entityt> abst_arrays;
-    // std::vector<entityt> abst_arrays;
 
     //Index vars to be abstracted
     std::unordered_map<irep_idt, entityt> abst_indices;
-    // std::vector<entityt> abst_indices;
+    
+    //Length vars to be abstracted
+    std::unordered_map<irep_idt, entityt> abst_lengths;
 
     // Shape of the abstraction
     abst_shapet shape;
@@ -156,6 +162,7 @@ class abstraction_spect
       : abst_func_file(_spec.abst_func_file),
         abst_arrays(_spec.abst_arrays),
         abst_indices(_spec.abst_indices),
+        abst_lengths(_spec.abst_lengths),
         shape(_spec.shape), 
         is_precise_func(_spec.is_precise_func),
         compare_indices_func(_spec.compare_indices_func),
@@ -166,14 +173,18 @@ class abstraction_spect
     }
 
     //We will have functions for accessing and modifying the above data.
-    //array_or_index: false-array, true-index
-    void insert_entity(const irep_idt &_name, bool array_or_index)
+    //_type: "array", "scalar", "length"
+    void insert_entity(const irep_idt &_name, const std::string &_type)
     {
       entityt new_entity(_name);
-      if(!array_or_index)
+      if(_type == "array")
         abst_arrays.insert({_name, new_entity});
-      else
+      else if(_type == "scalar")
         abst_indices.insert({_name, new_entity});
+      else if(_type == "length")
+        abst_lengths.insert({_name, new_entity});
+      else
+        throw "Unknown entity type: " + _type;
     }
 
     const std::unordered_map<irep_idt, entityt> &get_abst_arrays() const
@@ -186,6 +197,11 @@ class abstraction_spect
       return abst_indices;
     }
 
+    const std::unordered_map<irep_idt, entityt> &get_abst_lengths() const
+    {
+      return abst_lengths;
+    }
+
     const bool has_entity(const irep_idt &entity_name) const
     {
       return (abst_arrays.find(entity_name) != abst_arrays.end()) ||
@@ -202,6 +218,11 @@ class abstraction_spect
       return (abst_indices.find(entity_name) != abst_indices.end());
     }
 
+    const irep_idt get_length_index_name() const
+    {
+      return shape.get_length_index_name();
+    }
+
     //set abst func file path
     void set_abst_func_file(const std::string &_abst_func_file)
     {