Merge pull request diffblue#162 from viktormalik/dynobj-management

Improve management of dynamic objects

Author: viktormalik

src/2ls/2ls_parse_options.cpp

@@ -55,6 +55,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include "graphml_witness_ext.h"
 #include <solver/summary_db.h>
 #include <ssa/dynobj_instance_analysis.h>
+#include <ssa/dynamic_objects.h>
 
 #include "2ls_parse_options.h"
 #include "summary_checker_ai.h"
@@ -76,8 +77,7 @@ twols_parse_optionst::twols_parse_optionst(int argc, const char **argv):
   messaget(ui_message_handler),
   ui_message_handler(cmdline, "2LS " TWOLS_VERSION),
   recursion_detected(false),
-  threads_detected(false),
-  dynamic_memory_detected(false)
+  threads_detected(false)
 {
 }
 
@@ -408,7 +408,7 @@ int twols_parse_optionst::doit()
   if(get_goto_program(options))
     return 6;
 
-  if(cmdline.isset("heap") && dynamic_memory_detected)
+  if(cmdline.isset("heap") && dynamic_objects->have_objects())
   {
     // Only use sympath domain if dynamic memory is used
     options.set_option("sympath", true);
@@ -430,6 +430,7 @@ int twols_parse_optionst::doit()
     irep_idt function=cmdline.get_value("function");
     show_ssa(
       goto_model,
+      *dynamic_objects,
       options,
       function,
       simplify,
@@ -441,15 +442,26 @@ int twols_parse_optionst::doit()
   if(cmdline.isset("show-defs"))
   {
     irep_idt function=cmdline.get_value("function");
-    show_defs(goto_model, function, options, std::cout, ui_message_handler);
+    show_defs(
+      goto_model,
+      function,
+      *dynamic_objects,
+      options,
+      std::cout,
+      ui_message_handler);
     return 7;
   }
 
   if(cmdline.isset("show-assignments"))
   {
     irep_idt function=cmdline.get_value("function");
     show_assignments(
-      goto_model, function, options, std::cout, ui_message_handler);
+      goto_model,
+      function,
+      *dynamic_objects,
+      options,
+      std::cout,
+      ui_message_handler);
     return 7;
   }
 
@@ -556,7 +568,7 @@ int twols_parse_optionst::doit()
       options.get_bool_option("incremental-bmc") ||
       options.get_unsigned_int_option("unwind")) &&
      !options.get_bool_option("nontermination") &&
-     dynamic_memory_detected)
+     dynamic_objects->have_objects())
   {
     status() << "Using GOTO unwinder due to presence of dynamic memory" << eom;
     options.set_option("unwind-goto", true);
@@ -566,7 +578,7 @@ int twols_parse_optionst::doit()
   if(options.get_bool_option("competition-mode") &&
      (options.get_bool_option("termination") ||
       options.get_bool_option("nontermination")) &&
-     dynamic_memory_detected)
+     dynamic_objects->have_objects())
   {
     error() << "Termination analysis does not support "
             << "dynamic memory allocation" << eom;
@@ -580,18 +592,18 @@ int twols_parse_optionst::doit()
     if(!options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_ait(options, goto_model));
+        new summary_checker_ait(options, goto_model, *dynamic_objects));
     if(options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_kindt(options, goto_model));
+        new summary_checker_kindt(options, goto_model, *dynamic_objects));
     if(!options.get_bool_option("k-induction") &&
        options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_bmct(options, goto_model));
+        new summary_checker_bmct(options, goto_model, *dynamic_objects));
     if(options.get_bool_option("nontermination"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_nontermt(options, goto_model));
+        new summary_checker_nontermt(options, goto_model, *dynamic_objects));
 
     checker->set_message_handler(get_message_handler());
     checker->simplify=!cmdline.isset("no-simplify");
@@ -613,7 +625,7 @@ int twols_parse_optionst::doit()
 
       if(out_file=="-")
       {
-        horn_encoding(goto_model, options, std::cout);
+        horn_encoding(goto_model, *dynamic_objects, options, std::cout);
       }
       else
       {
@@ -630,7 +642,7 @@ int twols_parse_optionst::doit()
           return 1;
         }
 
-        horn_encoding(goto_model, options, out);
+        horn_encoding(goto_model, *dynamic_objects, options, out);
       }
 
       return 0;
@@ -1110,8 +1122,8 @@ bool twols_parse_optionst::process_goto_program(
     goto_model.goto_functions.compute_loop_numbers();
 
     // Replace malloc
-    dynamic_memory_detected=replace_malloc(
-      goto_model, "", options.get_bool_option("pointer-check"));
+    dynamic_objects=util_make_unique<dynamic_objectst>(goto_model);
+    dynamic_objects->replace_malloc(options.get_bool_option("pointer-check"));
 
     // Allow recording of mallocs and memory leaks
     if(options.get_bool_option("pointer-check"))
@@ -1136,7 +1148,7 @@ bool twols_parse_optionst::process_goto_program(
       inline_main(goto_model);
     }
 
-    auto dynobj_instances=split_dynamic_objects(goto_model, options);
+    dynamic_objects->generate_instances(options);
 
     if(!cmdline.isset("independent-properties"))
     {

src/2ls/2ls_parse_options.h

@@ -17,7 +17,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/replace_symbol.h>
 
 #include <analyses/goto_check.h>
-#include <ssa/dynobj_instance_analysis.h>
+#include <ssa/dynamic_objects.h>
 
 class goto_modelt;
 class optionst;
@@ -83,7 +83,8 @@ class twols_parse_optionst:
   ui_message_handlert ui_message_handler;
   bool recursion_detected;
   bool threads_detected;
-  bool dynamic_memory_detected;
+  std::unique_ptr<dynamic_objectst> dynamic_objects;
+
   virtual void register_languages();
 
   void get_command_line_options(optionst &options);
@@ -180,18 +181,6 @@ class twols_parse_optionst:
   void add_dynamic_object_rec(exprt &expr, symbol_tablet &symbol_table);
   void split_same_symbolic_object_assignments(goto_modelt &goto_model);
   void remove_dead_goto(goto_modelt &goto_model);
-  void compute_dynobj_instances(
-    const goto_programt &goto_program,
-    const dynobj_instance_analysist &analysis,
-    std::map<symbol_exprt, size_t> &instance_counts,
-    const namespacet &ns);
-  void create_dynobj_instances(
-    goto_programt &goto_program,
-    const std::map<symbol_exprt, size_t> &instance_counts,
-    symbol_tablet &symbol_table);
-  std::map<symbol_exprt, size_t> split_dynamic_objects(
-    goto_modelt &goto_model,
-    const optionst &options);
   void limit_array_bounds(goto_modelt &goto_model);
   void memory_assert_info(goto_modelt &goto_model);
   void handle_freed_ptr_compare(goto_modelt &goto_model);

src/2ls/horn_encoding.cpp

@@ -22,11 +22,13 @@ class horn_encodingt
 public:
   horn_encodingt(
     const goto_modelt &_goto_model,
+    dynamic_objectst &_dynamic_objects,
     const optionst &_options,
     std::ostream &_out):
     goto_functions(_goto_model.goto_functions),
     symbol_table(_goto_model.symbol_table),
     ns(_goto_model.symbol_table),
+    dynamic_objects(_dynamic_objects),
     options(_options),
     out(_out),
     smt2_conv(ns, "", "Horn-clause encoding", "", smt2_convt::solvert::Z3, _out)
@@ -39,6 +41,7 @@ class horn_encodingt
   const goto_functionst &goto_functions;
   const symbol_tablet &symbol_table;
   const namespacet ns;
+  dynamic_objectst &dynamic_objects;
   const optionst &options;
   std::ostream &out;
 
@@ -66,7 +69,13 @@ void horn_encodingt::translate(
          ";\n";
 
   // compute SSA
-  local_SSAt local_SSA(function_id, function, symbol_table, options, "");
+  local_SSAt local_SSA(
+    function_id,
+    function,
+    symbol_table,
+    dynamic_objects,
+    options,
+    "");
 
   const goto_programt &body=function.body;
 
@@ -214,8 +223,9 @@ void horn_encodingt::translate(
 
 void horn_encoding(
   const goto_modelt &goto_model,
+  dynamic_objectst &dynamic_objects,
   const optionst &options,
   std::ostream &out)
 {
-  horn_encodingt(goto_model, options, out)();
+  horn_encodingt(goto_model, dynamic_objects, options, out)();
 }

src/2ls/horn_encoding.h

@@ -17,7 +17,8 @@ Module: Horn-clause Encoding
 #include <goto-programs/goto_model.h>
 
 void horn_encoding(
-  const goto_modelt &,
+  const goto_modelt &goto_model,
+  dynamic_objectst &dynamic_objects,
   const optionst &options,
   std::ostream &out);
 

src/2ls/preprocessing_util.cpp

@@ -518,153 +518,6 @@ void twols_parse_optionst::remove_dead_goto(goto_modelt &goto_model)
   }
 }
 
-/// For each allocation site, compute the number of objects that must be used to
-/// soundly represent all objects allocated at the given site.
-void twols_parse_optionst::compute_dynobj_instances(
-  const goto_programt &goto_program,
-  const dynobj_instance_analysist &analysis,
-  std::map<symbol_exprt, size_t> &instance_counts,
-  const namespacet &ns)
-{
-  forall_goto_program_instructions(it, goto_program)
-  {
-    auto &analysis_value=analysis[it];
-    for(auto &obj : analysis_value.live_pointers)
-    {
-      auto must_alias=analysis_value.must_alias_relations.find(obj.first);
-      if(must_alias==analysis_value.must_alias_relations.end())
-        continue;
-
-      std::set<size_t> alias_classes;
-      for(auto &expr : obj.second)
-      {
-        size_t n;
-        const auto number=must_alias->second.data.get_number(expr);
-        if(!number)
-          continue;
-        n=*number;
-        alias_classes.insert(must_alias->second.data.find_number(n));
-      }
-
-      if(instance_counts.find(obj.first)==instance_counts.end() ||
-         instance_counts.at(obj.first)<alias_classes.size())
-      {
-        instance_counts[obj.first]=alias_classes.size();
-      }
-    }
-  }
-}
-
-/// For each allocation site, split the allocated abstract dynamic object into
-/// multiple in order to preserve soundness of the analysis.
-void twols_parse_optionst::create_dynobj_instances(
-  goto_programt &goto_program,
-  const std::map<symbol_exprt, size_t> &instance_counts,
-  symbol_tablet &symbol_table)
-{
-  Forall_goto_program_instructions(it, goto_program)
-  {
-    if(it->is_assign())
-    {
-      auto &assign=to_code_assign(it->code_nonconst());
-      if(assign.rhs().get_bool("#malloc_result"))
-      {
-        exprt &rhs=assign.rhs();
-        exprt &abstract_obj=rhs.id()==ID_if ? to_if_expr(rhs).false_case()
-                                            : rhs;
-        exprt &address=abstract_obj.id()==ID_typecast ?
-                       to_typecast_expr(abstract_obj).op() : abstract_obj;
-        if(address.id()!=ID_address_of)
-          continue;
-        exprt &obj=to_address_of_expr(address).object();
-        if(obj.id()!=ID_symbol)
-          continue;
-
-        if(obj.get_bool("#concrete"))
-          continue;
-
-        if(instance_counts.find(to_symbol_expr(obj))==instance_counts.end())
-          continue;
-
-        size_t count=instance_counts.at(to_symbol_expr(obj));
-        if(count<=1)
-          continue;
-
-        symbolt obj_symbol=
-          symbol_table.get_writeable_ref(to_symbol_expr(obj).get_identifier());
-
-        const std::string name=id2string(obj_symbol.name);
-        const std::string base_name=id2string(obj_symbol.base_name);
-        std::string suffix="$"+std::to_string(0);
-
-        obj_symbol.name=name+suffix;
-        obj_symbol.base_name=base_name+suffix;
-        symbol_table.add(obj_symbol);
-
-        exprt new_rhs=address_of_exprt(obj_symbol.symbol_expr());
-        if(abstract_obj.id()==ID_typecast)
-          new_rhs=typecast_exprt(new_rhs, rhs.type());
-        new_rhs.set("#malloc_result", true);
-
-        for(size_t i=1; i<count; ++i)
-        {
-          symbolt nondet;
-          nondet.type=bool_typet();
-          nondet.name="$guard#os"+std::to_string(it->location_number)+"#"+
-                      std::to_string(i);
-          nondet.base_name=nondet.name;
-          nondet.pretty_name=nondet.name;
-          symbol_table.add(nondet);
-
-          const exprt nondet_bool_expr =
-            side_effect_expr_nondett(bool_typet(), it->source_location);
-          goto_program.insert_before(
-            it,
-            goto_programt::make_assignment(
-              code_assignt(nondet.symbol_expr(), nondet_bool_expr),
-              it->source_location));
-
-          suffix="$"+std::to_string(i);
-          obj_symbol.name=name+suffix;
-          obj_symbol.base_name=base_name+suffix;
-
-          exprt new_obj=address_of_exprt(obj_symbol.symbol_expr());
-          if(abstract_obj.id()==ID_typecast)
-            new_obj=typecast_exprt(new_obj, rhs.type());
-          new_rhs=if_exprt(
-            nondet.symbol_expr(), new_obj, new_rhs);
-          new_rhs.set("#malloc_result", true);
-        }
-
-        abstract_obj=new_rhs;
-        abstract_obj.set("#malloc_result", true);
-      }
-    }
-  }
-}
-
-std::map<symbol_exprt, size_t> twols_parse_optionst::split_dynamic_objects(
-  goto_modelt &goto_model,
-  const optionst &options)
-{
-  std::map<symbol_exprt, size_t> dynobj_instances;
-  for(auto &f_it : goto_model.goto_functions.function_map)
-  {
-    if(!f_it.second.body_available())
-      continue;
-    namespacet ns(goto_model.symbol_table);
-    ssa_value_ait value_analysis(f_it.first, f_it.second, ns, options);
-    dynobj_instance_analysist do_inst(
-      f_it.first, f_it.second, ns, options, value_analysis);
-
-    compute_dynobj_instances(
-      f_it.second.body, do_inst, dynobj_instances, ns);
-    create_dynobj_instances(
-      f_it.second.body, dynobj_instances, goto_model.symbol_table);
-  }
-  return dynobj_instances;
-}
-
 /// Assert size of static arrays to be max 50000.
 void twols_parse_optionst::limit_array_bounds(goto_modelt &goto_model)
 {