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

abstraction: put all functions into one namespace/class

Author: Lefan Zhang

regression/abstraction/specs/aws_array_eq_c_str.json

@@ -1,41 +1,43 @@
 {
     "entries": [
         {
-            "entity": "string",
+            "entity": "array",
             "function": "aws_array_eq_c_str_harness",
-            "name": "aws_array_eq_c_str_harness::1::c_str",
+            "name": "aws_array_eq_c_str_harness::1::array",
             "shape": {
-                "indices": ["cncrt", "clast"],
+                "indices": ["cncrt0", "cncrt", "length"],
                 "assumptions": [
-                    "cncrt < clast"
+                    "cncrt0==0",
+                    "cncrt0<cncrt",
+                    "cncrt<length"
                 ],
-                "shape-type": "*c*c"
+                "shape-type": "c*c*l*"
             },
-            "abst-function-file": "./abst-funcs.c",
+            "abst-function-file": "../abst-funcs.c",
             "abst-functions":{
-                "add-abs-conc": "add_abs_to_conc",
-                "sub-abs-conc": "sub_conc_from_abs",
-                "precise-check": "is_precise",
-                "abstract-index": "two_abs",
-                "concretize-index": "concretize",
+                "add-abs-conc": "add_abs_to_conc_3",
+                "sub-abs-conc": "sub_conc_from_abs_3",
+                "precise-check": "is_precise_3",
+                "abstract-index": "three_abs",
+                "concretize-index": "concretize_3",
                 "multiply-indices": null,
                 "mod-indices": null
             },
             "related-entities": [
                 {
                     "entity": "array",
                     "function": "aws_array_eq_c_str_harness",
-                    "name": "aws_array_eq_c_str_harness::1::array"
+                    "name": "aws_array_eq_c_str_harness::1::c_str"
                 },
                 {
-                    "entity": "scalar",
+                    "entity": "length",
                     "function": "aws_array_eq_c_str_harness",
                     "name": "aws_array_eq_c_str_harness::1::array_len"
                 },
                 {
                     "entity": "scalar",
-                    "function": "aws_array_eq_c_str_harness",
-                    "name": "aws_array_eq_c_str_harness::1::str_len"
+                    "function": "",
+                    "name": "str_len"
                 }
             ]
 

src/goto-instrument/abstraction.cpp

@@ -23,19 +23,19 @@ Author: Lefan Zhang, [email protected]
 #include <linking/static_lifetime_init.h>
 #include "abstraction.h"
 
-void expr_type_relation::link(size_t i1, size_t i2)
+void am_abstractiont::expr_type_relation::link(size_t i1, size_t i2)
 {
   edges[i1].push_back(i2);
   edges[i2].push_back(i1);
 }
 
-void expr_type_relation::link_array(size_t i1, size_t i2)
+void am_abstractiont::expr_type_relation::link_array(size_t i1, size_t i2)
 {
   edges_array[i1].push_back(i2);
   edges_array[i2].push_back(i1);
 }
 
-size_t expr_type_relation::add_expr(const exprt &expr)
+size_t am_abstractiont::expr_type_relation::add_expr(const exprt &expr)
 {
   size_t index = expr_list.size();
   expr_list.push_back(expr);
@@ -110,7 +110,7 @@ size_t expr_type_relation::add_expr(const exprt &expr)
   return index;
 }
 
-void expr_type_relation::solve()
+void am_abstractiont::expr_type_relation::solve()
 {
   while(!todo.empty())
   {
@@ -141,7 +141,7 @@ void expr_type_relation::solve()
   }
 }
 
-void expr_type_relation::solve_array()
+void am_abstractiont::expr_type_relation::solve_array()
 {
   while(!todo_array.empty())
   {
@@ -172,15 +172,15 @@ void expr_type_relation::solve_array()
   }
 }
 
-void link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_spec, ui_message_handlert &msg_handler, const optionst &options)
+void am_abstractiont::link_abst_functions(goto_modelt &goto_model, const abstraction_spect &abst_spec, ui_message_handlert &msg_handler, const optionst &options)
 {
   std::vector<std::string> abstfiles = abst_spec.get_abstraction_function_files();  // get abst function file names
   goto_modelt goto_model_for_abst_fns = initialize_goto_model(abstfiles, msg_handler, options);  // read files
   link_goto_model(goto_model, goto_model_for_abst_fns, msg_handler);  // link goto model
 }
 
 const std::tuple<std::unordered_set<irep_idt>, std::unordered_set<irep_idt>>
-find_index_symbols(
+am_abstractiont::find_index_symbols(
   const goto_functiont &goto_function,
   const irep_idt &array_name)
 {
@@ -286,7 +286,7 @@ find_index_symbols(
   return result;
 }
 
-void complete_abst_spec(const goto_functiont& goto_function, abstraction_spect &abst_spec)
+void am_abstractiont::complete_abst_spec(const goto_functiont& goto_function, abstraction_spect &abst_spec)
 {
   for(auto &spec: abst_spec.get_specs())
   {
@@ -327,7 +327,7 @@ irep_idt check_expr_is_symbol(const exprt &expr)
 
 // go into a function to find all function calls we'll need to abstract
 std::vector<std::tuple<irep_idt, std::unordered_map<irep_idt, irep_idt>>>
-find_function_calls(irep_idt func_name, goto_modelt &goto_model, const abstraction_spect &abst_spec)
+am_abstractiont::find_function_calls(irep_idt func_name, goto_modelt &goto_model, const abstraction_spect &abst_spec)
 {
   std::vector<std::tuple<irep_idt, std::unordered_map<irep_idt, irep_idt>>> result;
 
@@ -359,7 +359,7 @@ find_function_calls(irep_idt func_name, goto_modelt &goto_model, const abstracti
 }
 
 std::unordered_map<irep_idt, abstraction_spect> 
-calculate_complete_abst_specs_for_funcs(goto_modelt &goto_model, abstraction_spect &abst_spec)
+am_abstractiont::calculate_complete_abst_specs_for_funcs(goto_modelt &goto_model, abstraction_spect &abst_spec)
 {
   std::unordered_map<irep_idt, abstraction_spect> function_spec_map;  // map from function to its abst_spec
   const goto_functiont &init_function = goto_model.get_goto_function(abst_spec.get_func_name());
@@ -423,7 +423,7 @@ calculate_complete_abst_specs_for_funcs(goto_modelt &goto_model, abstraction_spe
   return function_spec_map;
 }
 
-bool contains_an_entity_to_be_abstracted(const exprt &expr, const abstraction_spect &abst_spec)
+bool am_abstractiont::contains_an_entity_to_be_abstracted(const exprt &expr, const abstraction_spect &abst_spec)
 {
   struct match_abst_symbolt
   {
@@ -444,12 +444,12 @@ bool contains_an_entity_to_be_abstracted(const exprt &expr, const abstraction_sp
 
 }
 
-irep_idt get_abstract_name(const irep_idt &old_name)
+irep_idt am_abstractiont::get_abstract_name(const irep_idt &old_name)
 {
   return irep_idt(std::string(old_name.c_str())+"$abst");
 }
 
-bool contains_a_function_call(const exprt &expr)
+bool am_abstractiont::contains_a_function_call(const exprt &expr)
 {
   class find_functiont : public const_expr_visitort
   {
@@ -473,7 +473,7 @@ bool contains_a_function_call(const exprt &expr)
   return ff.found;
 }
 
-std::vector<exprt> get_direct_access_exprs(const exprt &expr, const abstraction_spect::spect &spec)
+std::vector<exprt> am_abstractiont::get_direct_access_exprs(const exprt &expr, const abstraction_spect::spect &spec)
 {
   class find_direct_accesst : public const_expr_visitort
   {
@@ -518,7 +518,7 @@ std::vector<exprt> get_direct_access_exprs(const exprt &expr, const abstraction_
   return result;
 }
 
-exprt add_guard_expression_to_assert(
+exprt am_abstractiont::add_guard_expression_to_assert(
   const exprt &expr,
   const exprt &expr_before_abst,
   const abstraction_spect &abst_spec,
@@ -581,7 +581,7 @@ exprt add_guard_expression_to_assert(
   }
 }
 
-void declare_abst_variables_for_func(
+void am_abstractiont::declare_abst_variables_for_func(
   goto_modelt &goto_model,
   const irep_idt &func_name,
   const abstraction_spect &abst_spec,
@@ -676,7 +676,7 @@ void declare_abst_variables_for_func(
   }
 }
 
-bool check_if_exprt_eval_to_abst_index(
+bool am_abstractiont::check_if_exprt_eval_to_abst_index(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   abstraction_spect::spect &spec)
@@ -763,7 +763,7 @@ bool check_if_exprt_eval_to_abst_index(
   }
 }
 
-symbolt create_function_call(
+symbolt am_abstractiont::create_function_call(
   const irep_idt &func_name,
   const exprt::operandst operands,
   const irep_idt &caller, 
@@ -830,7 +830,7 @@ symbolt create_function_call(
   return new_symb;
 }
 
-exprt abstract_expr_write(
+exprt am_abstractiont::abstract_expr_write(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   const goto_modelt &goto_model,
@@ -871,7 +871,7 @@ exprt abstract_expr_write(
   }
 }
 
-exprt create_comparator_expr_abs_abs(
+exprt am_abstractiont::create_comparator_expr_abs_abs(
   const exprt &orig_expr,
   const abstraction_spect::spect &spec,
   const goto_modelt &goto_model,
@@ -906,7 +906,7 @@ exprt create_comparator_expr_abs_abs(
   return std::move(result_expr);
 }
 
-exprt abstract_expr_read_comparator(
+exprt am_abstractiont::abstract_expr_read_comparator(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   const goto_modelt &goto_model,
@@ -1022,7 +1022,7 @@ exprt abstract_expr_read_comparator(
 }
 
 // check whether an expr is a pointer offset
-bool is_pointer_offset(const exprt &expr)
+bool am_abstractiont::is_pointer_offset(const exprt &expr)
 {
   if(expr.id() == ID_pointer_offset)
   {
@@ -1039,7 +1039,7 @@ bool is_pointer_offset(const exprt &expr)
   }
 }
 
-exprt abstract_expr_read_plusminus(
+exprt am_abstractiont::abstract_expr_read_plusminus(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   const goto_modelt &goto_model,
@@ -1111,7 +1111,7 @@ exprt abstract_expr_read_plusminus(
   }
 }
 
-exprt abstract_expr_read_dereference(
+exprt am_abstractiont::abstract_expr_read_dereference(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   const goto_modelt &goto_model,
@@ -1215,7 +1215,7 @@ exprt abstract_expr_read_dereference(
   }
 }
 
-exprt abstract_expr_read(
+exprt am_abstractiont::abstract_expr_read(
   const exprt &expr,
   const abstraction_spect &abst_spec,
   const goto_modelt &goto_model,
@@ -1293,7 +1293,7 @@ exprt abstract_expr_read(
   }
 }
 
-void define_concrete_indices(goto_modelt &goto_model, const abstraction_spect &abst_spec)
+void am_abstractiont::define_concrete_indices(goto_modelt &goto_model, const abstraction_spect &abst_spec)
 {
   for(const auto &spec: abst_spec.get_specs())
   {
@@ -1333,10 +1333,8 @@ void define_concrete_indices(goto_modelt &goto_model, const abstraction_spect &a
   }
 }
 
-void insert_shape_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec)
+void am_abstractiont::insert_shape_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec)
 {
-
-
   namespacet ns(goto_model.get_symbol_table());
   for(const auto &spec: abst_spec.get_specs())
   {
@@ -1359,7 +1357,7 @@ void insert_shape_assumptions(goto_modelt &goto_model, const abstraction_spect &
   }
 }
 
-void add_length_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec)
+void am_abstractiont::add_length_assumptions(goto_modelt &goto_model, const abstraction_spect &abst_spec)
 {
   for(const auto &spec: abst_spec.get_specs())
   {
@@ -1447,7 +1445,7 @@ void add_length_assumptions(goto_modelt &goto_model, const abstraction_spect &ab
   }
 }
 
-void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec)
+void am_abstractiont::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);
@@ -1559,6 +1557,7 @@ void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec
           new_rhs = as.rhs();
         }
 
+        // TODO: when lhs and rhs are not both abstracted, we should do the translation.
         code_assignt new_as(new_lhs, new_rhs);
         it->set_assign(new_as);
       }
@@ -1577,7 +1576,7 @@ void abstract_goto_program(goto_modelt &goto_model, abstraction_spect &abst_spec
       if(
         !it->is_decl() && !it->is_end_function() && !it->is_goto() &&
         !it->is_return() && !it->is_function_call() && !it->is_assert() &&
-        !it->is_assign() && !it->is_assume() && !it->is_dead())
+        !it->is_assign() && !it->is_assume() && !it->is_dead() && !it->is_skip())
         throw "Unknown instruction type " + std::to_string(it->type);
 
       // insert new instructions before it