Fix the update happening in function call problem

Author: zhixing-xu

regression/cbmc/Abstract-loops3/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+#define ROW 10
+
+void boo(int* x)
+{
+  *x = *x + 1;
+}
+
+
+void main()
+{
+  int *x = (int*)malloc(sizeof(int));
+  int buffer[ROW];
+  *x = 2;
+  // not shrinkable since x has a self-update in boo()
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(x);
+    buffer[*x] = 1;
+  }
+}

regression/cbmc/Abstract-loops3/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset main.0
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrinked (so 
+they appears in unwinding). Even when the instruction that makes the loop
+unshrinkable is in another function

regression/goto-instrument/abstract-loops3/main.c

@@ -1,6 +1,5 @@
 #include <stdlib.h>
-#define ROW 3
-#define COL 10
+#define ROW 10
 
 void boo(int* x)
 {
@@ -12,11 +11,11 @@ void main()
 {
   int *x = (int*)malloc(sizeof(int));
   int buffer[ROW];
-  // not shrinkable since x is used in mem-safe assertion in boo()
-  // and r update itself in loop
+  *x = 2;
+  // not shrinkable since x has a self-update in boo()
   for(int i = 0; i < ROW; i++)
   {
     boo(x);
-    buffer[*x];
+    buffer[*x] = 1;
   }
 }

regression/goto-instrument/abstract-loops3/test.desc

@@ -1,22 +1,15 @@
-KNOWNBUG
+CORE
 main.c
---bounds-check --pointer-check --abstract-loops --abstractset boo.0,main.0
+--bounds-check --pointer-check --add-library --abstract-loops --abstractset main.0
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 main\.0
-main\.1
-ASSUME j < 10
-ASSUME j >= 0
 --
-boo\.0
 ASSUME i < 10
 ASSUME i >= 0
 ^warning: ignoring
 --
 This test ensures that the loops with loop variable i are not shrinked (so 
-they appears in unwinding). Although the second loop in main is shrinkable, but
-it's not in the target loop set provided by --abstractset, so it shouldn't be
-shrinked. 
-It also ensures the loop in boo() with loop variable j is shrinked and the 
-constraints are correctly applied. 
+they appears in unwinding). Even when the instruction that makes the loop
+unshrinkable is in another function

src/goto-instrument/abstract_loops.cpp

@@ -20,11 +20,11 @@ Author: Zhixing Xu, [email protected]
 #include <analyses/goto_rw.h>
 
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/cfg.h>
 
 // debug
 #ifdef DEBUG_ABSTRACT_LOOPS
 #include "iostream"
-#include <util/expr_iterator.h>
 #endif
 
 class abstract_loopst
@@ -43,6 +43,8 @@ class abstract_loopst
     dependence_grapht dep_graph(_ns);
     // data structures initialization
     dep_graph(goto_model.goto_functions, _ns);
+    // build the CFG data structure
+    cfg(goto_model.goto_functions);
     // call main function
     abstract_loops(goto_model, dep_graph, target_loop_map);
   }
@@ -53,8 +55,8 @@ class abstract_loopst
   // target abstract loop number for each function
   loop_mapt target_loop_map;
   // set of all leaf dependency nodes for loop variables
-  nodeset leaf_nodes;
-  nodeset update_nodes;
+  //nodeset leaf_nodes;
+  //nodeset update_nodes;
   // current function
   irep_idt fn;
   // map from instruction line # to the set of loops it belongs to
@@ -65,6 +67,18 @@ class abstract_loopst
   typedef dep_graph_domaint::depst depst;
   // name space for program
   const namespacet ns;
+  // cfg
+  struct cfg_nodet
+  {
+    cfg_nodet():node_required(false)
+    {
+    }
+
+    bool node_required;
+  };
+
+  typedef cfg_baset<cfg_nodet> cfgt;
+  cfgt cfg;
 
   // functions in this class
   void abstract_loops(goto_modelt &goto_model,
@@ -75,7 +89,8 @@ class abstract_loopst
 
   void update_shrinkability(unsigned loc, irep_idt func);
 
-  void check_assertion(unsigned location, const dependence_grapht &dep_graph);
+  void check_assertion(unsigned location, const dependence_grapht &dep_graph,
+      const goto_functionst &goto_functions);
 
   void abstract_goto_program(unsigned loop_num,
     const dependence_grapht &dep_graph,
@@ -185,6 +200,7 @@ class abstract_loopst
 }; // end of class abstract_loopst
 
 
+#ifdef DEBUG_ABSTRACT_LOOPS
 /// print out nodes in set
 void print_nodes(abstract_loopst::nodeset &node_set)
 {
@@ -198,6 +214,7 @@ void print_nodes(abstract_loopst::nodeset &node_set)
   }
   std::cout << '\n';
 }
+#endif
 
 /// Do the abstraction on goto program (modify goto program)
 /// \param loop_num: target loop number
@@ -241,16 +258,10 @@ void abstract_loopst::abstract_goto_program(unsigned loop_num,
   f_it = goto_functions.function_map.find(fn);
   i_it = f_it->second.body.instructions.begin();
   std::advance(i_it, loop_info->init_loc - i_it->location_number);
-
-  //init values can be nondet
-  const code_assignt &code_assign = to_code_assign(i_it->code);
-  if(!(code_assign.rhs().id() == ID_side_effect))
-  {
-    expr = i_it->code;
-    expr.id(is_inc ? ID_ge : ID_le);
-    expr.type().id(ID_bool);
-    i_it->make_assumption(expr);
-  }
+  expr = i_it->code;
+  expr.id(is_inc ? ID_ge : ID_le);
+  expr.type().id(ID_bool);
+  i_it->make_assumption(expr);
 
   // change loop head into assumption, skip goto at loop end
   loop_info->build_assumption();
@@ -276,7 +287,7 @@ void abstract_loopst::update_shrinkability(unsigned loc, irep_idt func)
 /// \param location: line number for assertion
 /// \param dep_graph: dependency graph for the program
 void abstract_loopst::check_assertion(unsigned location,
-  const dependence_grapht &dep_graph)
+  const dependence_grapht &dep_graph, const goto_functionst &goto_functions)
 {
 #ifdef DEBUG_ABSTRACT_LOOPS
   std::cout << "Check assertion at: " << location << "\n";
@@ -339,6 +350,18 @@ void abstract_loopst::check_assertion(unsigned location,
   print_nodes(update_set);
 #endif
 
+  // node set
+  nodeset leaf_nodes;
+  nodeset update_nodes;
+  for(auto loop_n: insloop_map[location])
+  {
+    irep_idt func = dep_graph[location].PC->function;
+    abstract_loopt *loop_info = &(absloop_map[func].find(loop_n)->second);
+    leaf_nodes.insert(loop_info->var_leaves.begin(),
+        loop_info->var_leaves.end());
+    update_nodes.insert(loop_info->var_updates.begin(),
+        loop_info->var_updates.end());
+  }
   // check dependence of leaf set
   nodeset diff;
   std::set_difference(leaf_set.begin(), leaf_set.end(),
@@ -358,13 +381,39 @@ void abstract_loopst::check_assertion(unsigned location,
   {
     if(is_in_cycle(loc, dep_graph))
     {
-      update_shrinkability(loc, dep_graph[loc].PC->function);
+      nodeset entry_set;
+      std::queue<unsigned> entry_queue;
+      add_to_queue(entry_set, entry_queue, loc);
+      while(!entry_queue.empty())
+      {
+        unsigned node = entry_queue.front();
+        entry_queue.pop();
+        update_shrinkability(node, dep_graph[node].PC->function);
+        // check loops calling this function call
+        goto_functionst::function_mapt::const_iterator f_it=
+          goto_functions.function_map.find(dep_graph[node].PC->function);
+
+        goto_programt::const_targett begin_function=
+          f_it->second.body.instructions.begin();
+
+        cfgt::entry_mapt::const_iterator entry=
+          cfg.entry_map.find(begin_function);
+        if(entry!=cfg.entry_map.end())
+        {
+          for(cfgt::edgest::const_iterator
+              it=cfg[entry->second].in.begin();
+              it!=cfg[entry->second].in.end();
+              ++it)
+          {
+            add_to_queue(entry_set, entry_queue, it->first);
+          }
+        }
+      }
     }
     else
     {
       // check if the update depends on loop variable
       const goto_programt::instructiont &inst = *(dep_graph[loc].PC);
-      std::cout << "check location " << loc << " type " << inst.type << "\n";
       if(!inst.is_assign())
         continue;
       value_setst &value_sets=
@@ -496,34 +545,34 @@ void abstract_loopst::get_loop_info(
     return;
   }
 
+  // This is for SVcomp cases where values can be nondet
+  const code_assignt &code_assign =
+    to_code_assign(dep_graph[loop_info.init_loc].PC->code);
+  if(code_assign.rhs().id() == ID_side_effect)
+  {
+#ifdef DEBUG_ABSTRACT_LOOPS
+    std::cout << "Unshrinkable: Loop variable init to nondet\n";
+#endif
+    return;
+  }
+
 #ifdef DEBUG_ABSTRACT_LOOPS
   std::cout << "  Leaf dependency nodes for loop variable: ";
   print_nodes(loop_info.var_leaves);
   std::cout << "  Update node for loop variable: ";
   print_nodes(loop_info.var_updates);
 #endif
 
-  //// This is for SVcomp cases where values can be nondet
-  //const code_assignt &code_assign =
-    //to_code_assign(dep_graph[loop_info.init_loc].PC->code);
-  //if(code_assign.rhs().id() == ID_side_effect)
-  //{
-//#ifdef DEBUG_ABSTRACT_LOOPS
-    //std::cout << "Unshrinkable: Loop variable init to nondet\n";
-//#endif
-    //return;
-  //}
-
   // add to the instruction # -> loop # map
   // unsafe with function call, further check when doing abstraction
   for(unsigned n = head->location_number;
       n <= last->location_number; n++)
     insloop_map[n].insert(last->loop_number);
 
   absloop_map[fn].insert(loopnum_pair(last->loop_number, loop_info));
-  leaf_nodes.insert(loop_info.var_leaves.begin(), loop_info.var_leaves.end());
-  update_nodes.insert(loop_info.var_updates.begin(),
-      loop_info.var_updates.end());
+  //leaf_nodes.insert(loop_info.var_leaves.begin(), loop_info.var_leaves.end());
+  //update_nodes.insert(loop_info.var_updates.begin(),
+      //loop_info.var_updates.end());
 }
 
 /// Main function for abstraction, has 3 iterations to
@@ -557,7 +606,8 @@ void abstract_loopst::abstract_loops(goto_modelt &goto_model,
       Forall_goto_program_instructions(i_it, it->second.body)
       {
         if(i_it->is_assert())
-          check_assertion(i_it->location_number, dep_graph);
+          check_assertion(i_it->location_number, dep_graph,
+              goto_model.goto_functions);
       }
     }
   }