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

need_abst: implementation and tests; previous PR: fix 3 comments

Author: Lefan Zhang

src/goto-instrument/abstraction.cpp

@@ -15,6 +15,8 @@ Author: Lefan Zhang, [email protected]
 #include <queue>
 
 #include <util/std_expr.h>
+#include <util/expr_util.h>
+#include <util/format_expr.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_goto_model.h>
 
@@ -206,7 +208,6 @@ const std::unordered_set<irep_idt> find_index_symbols(const goto_functiont &goto
     if(it->is_function_call())
     {
       const code_function_callt fc = it->get_function_call();
-      code_function_callt::argumentst new_arguments = fc.arguments();
       exprt new_lhs = fc.lhs();
       etr.add_expr(fc.lhs());
 
@@ -232,7 +233,7 @@ void complete_abst_spec(const goto_functiont& goto_function, abstraction_spect &
   {
     for(const auto &ent: spec.get_abst_arrays())
       for(irep_idt index_name: find_index_symbols(goto_function, ent.first))
-        if(spec.get_abst_indices().find(index_name) != spec.get_abst_indices().end())
+        if(spec.get_abst_indices().find(index_name) == spec.get_abst_indices().end())
           spec.insert_entity(index_name, true);
   }
 }
@@ -274,18 +275,16 @@ find_function_calls(irep_idt func_name, goto_modelt &goto_model, const abstracti
       // it is a function call that we potentially need to abstract
       const code_function_callt fc = it->get_function_call();
       const irep_idt &new_func_name = to_symbol_expr(fc.function()).get_identifier();
+      const goto_functiont &new_function = goto_model.get_goto_function(new_func_name);
       std::unordered_map<irep_idt, irep_idt> map;
       for(size_t i=0; i<fc.arguments().size(); i++)
       {
         // for each argument, we check whether we need to abstract it.
         const exprt &arg = fc.arguments()[i];
         irep_idt symbol_name = check_expr_is_symbol(arg);
         if(symbol_name != "" && abst_spec.has_entity(symbol_name))
-        {
           // if so, we push it into the map
-          const goto_functiont &new_function = goto_model.get_goto_function(new_func_name);
           map.insert({symbol_name, new_function.parameter_identifiers[i]});
-        }
       }
       if(!map.empty())  //if map is not empty, we create a new entry in the result
         result.push_back(std::make_tuple(new_func_name, map));
@@ -340,11 +339,39 @@ calculate_complete_abst_specs_for_funcs(goto_modelt &goto_model, abstraction_spe
         complete_abst_spec(goto_model.get_goto_function(new_func_name), new_func_abst);
         function_spec_map.insert({new_func_name, new_func_abst});
       }
+      else
+      {
+        // we need to compare if the structure is the same
+        abstraction_spect new_func_abst = function_spec_map[current_func_name].update_abst_spec(current_func_name, new_func_name, name_pairs);
+        if(!new_func_abst.compare_shape(function_spec_map[new_func_name]))
+          throw "Same function abstracted with different shape!";
+      }
     }
   }
   return function_spec_map;
 }
 
+bool contains_an_abstracted_entity(const exprt &expr, const abstraction_spect &abst_spec)
+{
+  struct match_abst_symbolt
+  {
+    match_abst_symbolt(const abstraction_spect &_abst_spec) : abst_spec(_abst_spec) {}
+    // check if expr is an entity symbol that we want to abstract
+    bool operator()(const exprt &expr)
+    {
+      irep_idt symbol_name = check_expr_is_symbol(expr);
+      return symbol_name != "" && abst_spec.has_entity(symbol_name);
+    }
+  protected:
+    // we assume this abst_spec's life span covers 
+    // the life span of the match_abst_symbolt object
+    const abstraction_spect &abst_spec;
+  };
+  match_abst_symbolt match_abst_symbol(abst_spec);
+  return has_subexpr(expr, match_abst_symbol);
+
+}
+
 void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec)
 {
   // A couple of spects are initialized from the json file. We should go from there and insert spects to other functions
@@ -353,6 +380,37 @@ void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec
   for(auto &p: function_spec_map)
   {
     std::cout << "=========== " << p.first << " ===========" << std::endl;
+    std::cout << "----------- " << "Entities to be abstracted" << " -----------" << std::endl;
     p.second.print_entities();
+    std::cout << "----------- " << "Exprs containing the above entities" << " -----------" << std::endl;
+    const goto_functiont &goto_function = goto_model.get_goto_function(p.first);
+    const abstraction_spect &abst_spec = p.second;
+    forall_goto_program_instructions(it, goto_function.body)
+    {
+      // go through conditions
+      if(it->has_condition())
+        if(contains_an_abstracted_entity(it->get_condition(), abst_spec))
+          format_rec(std::cout, it->get_condition()) << std::endl;
+
+      // go through all expressions
+      if(it->is_function_call())
+      {
+        const code_function_callt fc = it->get_function_call();
+        if(contains_an_abstracted_entity(fc.lhs(), abst_spec))
+          format_rec(std::cout, fc.lhs()) << std::endl;
+        
+        for(const auto &arg : fc.arguments())
+          if(contains_an_abstracted_entity(arg, abst_spec))
+            format_rec(std::cout, arg) << std::endl;
+      }
+      else if(it->is_assign())
+      {
+        const code_assignt as = it->get_assign();
+        if(contains_an_abstracted_entity(as.lhs(), abst_spec))
+          format_rec(std::cout, as.lhs()) << std::endl;
+        if(contains_an_abstracted_entity(as.rhs(), abst_spec))
+          format_rec(std::cout, as.rhs()) << std::endl;
+      }
+    }
   }
 }

src/goto-instrument/abstraction.h

@@ -65,6 +65,11 @@ const std::unordered_set<irep_idt> find_index_symbols(const goto_functiont &goto
 std::unordered_map<irep_idt, abstraction_spect>
 calculate_complete_abst_specs_for_funcs(goto_modelt &goto_model, abstraction_spect &abst_spec);
 
+/// \param expr: the expression to be checked
+/// \param abst_spec: the abstraction_spect for the current function which contains all spects
+/// \return whether the expr contains an entity to be abstracted
+bool contains_an_abstracted_entity(const exprt &expr, const abstraction_spect &abst_spec);
+
 // abstract goto programs
 void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec);
 

src/goto-instrument/abstraction_spect.cpp

@@ -36,6 +36,17 @@ abstraction_spect::abstraction_spect(
       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");
     }
+    const auto &json_shape_obj = to_json_object(entry_obj.find("shape")->second);
+    const auto &json_shape_i_array = to_json_array(json_shape_obj.find("indices")->second);
+    const auto &json_shape_a_array = to_json_array(json_shape_obj.find("assumptions")->second);
+    std::vector<irep_idt> indices;
+    std::vector<std::string> assumptions;
+    for(auto it_i=json_shape_i_array.begin(); it_i != json_shape_i_array.end(); ++it_i)
+      indices.push_back(to_json_string(*it_i).value);
+    for(auto it_a=json_shape_a_array.begin(); it_a != json_shape_a_array.end(); ++it_a)
+      assumptions.push_back(to_json_string(*it_a).value);
+    std::string shape_type = to_json_string(json_shape_obj.find("shape-type")->second).value;
+    spec.set_shape(indices, assumptions, shape_type);
     specs.push_back(spec);
   }
 }
@@ -110,8 +121,13 @@ abstraction_spect abstraction_spect::update_abst_spec(
   new_abst_spec.function = new_function;
   for(const auto &spec: specs)
   {
-    new_abst_spec.specs.push_back(spec.update_abst_spec(old_function, new_function, _name_pairs));
+    spect new_spec = spec.update_abst_spec(old_function, new_function, _name_pairs);
+    if(!spec.compare_shape_only(new_spec))
+      throw "The updated spect's shape should be the same as the original one";
+    new_abst_spec.specs.push_back(new_spec);
   }
+  if(specs.size() != new_abst_spec.specs.size())
+    throw "The updated specs' size should remain the same";
   return new_abst_spec;
 }
 

src/goto-instrument/abstraction_spect.h

@@ -31,6 +31,52 @@ class abstraction_spect
   struct spect
   {
   public:
+    struct abst_shapet
+    {
+      std::vector<irep_idt> indices;
+      std::vector<std::string> assumptions;
+      std::string shape_type;  // e.g. "*cc*"
+    public:
+      abst_shapet() {}
+      abst_shapet(
+        std::vector<irep_idt> _indices,
+        std::vector<std::string> _assumptions,
+        std::string _shape_type)
+        : indices(_indices), assumptions(_assumptions), shape_type(_shape_type) {}
+      abst_shapet(const abst_shapet &other)
+        : indices(other.indices),
+          assumptions(other.assumptions),
+          shape_type(other.shape_type)
+      {
+      }
+      void add_index(const irep_idt &_index)
+      {
+        indices.push_back(_index);
+      }
+      void add_assumption(const std::string &_assumption)
+      {
+        assumptions.push_back(_assumption);
+      }
+      void set_shape_type(const std::string &_shape_type)
+      {
+        shape_type = _shape_type;
+      }
+      bool operator==(const abst_shapet &other) const
+      {
+        if(indices.size() != other.indices.size())
+          return false;
+        if(assumptions.size() != other.assumptions.size())
+          return false;
+        for(size_t i=0; i<indices.size(); i++)
+          if(indices[i] != other.indices[i])
+            return false;
+        for(size_t i=0; i<assumptions.size(); i++)
+          if(assumptions[i] != other.assumptions[i])
+            return false;
+        return (shape_type == other.shape_type);
+      }
+    };
+
     struct entityt
     {
       //Name of the array/list being abstracted
@@ -76,19 +122,8 @@ class abstraction_spect
     std::unordered_map<irep_idt, entityt> abst_indices;
     // std::vector<entityt> abst_indices;
 
-    //Names of references in increasing order
-    //Each ref is stored with path+name of the array being abstracted along
-    //with the name of ref itself (like c1, c2)
-    std::vector<entityt> refs_name;
-
-    //Assumptions on the references
-    std::vector<exprt> assumptions;
-
-    //List of variables directly indexing into array being abstracted.
-    //This list is required to handle while-loops correctly. Say ind indexes into array f
-    //and ind is used as iterator in the while loop. Then ind has to be abstracted ind-abs
-    //so as to reduce it's range from an potentially large value to a small abstract range.
-    std::vector<std::string> indices;
+    // Shape of the abstraction
+    abst_shapet shape;
 
     //Abstraction functions follow. These should be defined in the abstraction_funcs_file or
     //they are hard-coded ones. In abstraction_funcs_file function will begin with prefixes
@@ -109,9 +144,7 @@ class abstraction_spect
       : abst_func_file(_spec.abst_func_file),
         abst_arrays(_spec.abst_arrays),
         abst_indices(_spec.abst_indices),
-        refs_name(_spec.refs_name),
-        assumptions(_spec.assumptions),
-        indices(_spec.indices),
+        shape(_spec.shape), 
         is_precise_func(_spec.is_precise_func),
         compare_indices_func(_spec.compare_indices_func),
         addition_func(_spec.addition_func),
@@ -158,6 +191,33 @@ class abstraction_spect
       return abst_func_file;
     }
 
+    // set the shape
+    void set_shape(const std::vector<irep_idt> &indices, const std::vector<std::string> &assumptions, const std::string &shape_type)
+    {
+      shape = abst_shapet(indices, assumptions, shape_type);
+    }
+
+    // compare if two spect have the same abst shape
+    bool compare_shape(const spect &other) const
+    {
+      if(abst_arrays.size() != other.abst_arrays.size())
+        return false;
+      if(abst_indices.size() != other.abst_indices.size())
+        return false;
+      for(const auto &array: abst_arrays)
+        if(other.abst_arrays.find(array.first) == other.abst_arrays.end())
+          return false;
+      for(const auto &index: abst_indices)
+        if(other.abst_indices.find(index.first) == other.abst_indices.end())
+          return false;
+      return shape == other.shape;
+    }
+
+    bool compare_shape_only(const spect &other) const
+    {
+      return shape == other.shape;
+    }
+
     //We need to update the abstracted array/list/var names as we cross the function boundary.
     //For example, if function Foo has two arrays f1 and f2 that are abstracted.
     //Function Bar is defined as void Bar(array b1, array b2) and suppose Foo calls Bar(f1,f2).
@@ -199,6 +259,20 @@ class abstraction_spect
     return false;
   }
 
+  // compare if two spect have the same structure
+  bool compare_shape(const abstraction_spect &other) const
+  {
+    // In the update_abst_spec function, the result and the 
+    // original one should have the same spects in terms 
+    // of both order and shape
+    if(specs.size() != other.specs.size())
+      return false;
+    for(size_t i=0; i<specs.size(); i++)
+      if(!specs[i].compare_shape(other.specs[i]))
+        return false;
+    return true;
+  }
+
   // print all entities
   void print_entities() const;
 protected:

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -763,18 +763,6 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(cmdline.isset("use-abstraction"))
-    {
-      // std::string filename = cmdline.get_value("use-abstraction");
-      // jsont json;
-      // parse_json(filename, ui_message_handler, json);
-
-      // abstract_goto_program(goto_model, json);
-      std::cout << "abstract" << std::endl;
-
-      // return CPROVER_EXIT_SUCCESS;
-    }
-
     if(
       cmdline.isset("show-goto-functions") ||
       cmdline.isset("list-goto-functions"))