Update node only checks for lhs loop variable

Author: zhixing-xu

src/goto-instrument/abstract_loops.cpp

@@ -17,6 +17,7 @@ Author: Zhixing Xu, [email protected]
 
 #include <analyses/natural_loops.h>
 #include <analyses/dependence_graph.h>
+#include <analyses/goto_rw.h>
 
 #include <goto-programs/remove_skip.h>
 
@@ -240,10 +241,16 @@ 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);
-  expr = i_it->code;
-  expr.id(is_inc ? ID_ge : ID_le);
-  expr.type().id(ID_bool);
-  i_it->make_assumption(expr);
+
+  //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);
+  }
 
   // change loop head into assumption, skip goto at loop end
   loop_info->build_assumption();
@@ -295,6 +302,7 @@ void abstract_loopst::check_assertion(unsigned location,
         it != control_deps.end(); ++it)
     {
       add_to_queue(dep_set, dep_queue, (*it)->location_number);
+      ctrl_set.insert((*it)->location_number);
     }
   }
 
@@ -311,7 +319,7 @@ void abstract_loopst::check_assertion(unsigned location,
         add_to_queue(dep_set, dep_queue, (*it)->location_number);
         //if(is_in_cycle(node, dep_graph))
           //update_set.insert(node);
-        if(ctrl_set.find(node) != ctrl_set.end())
+        if(ctrl_set.find(node) == ctrl_set.end())
           update_set.insert(node);
       }
     else
@@ -338,18 +346,7 @@ void abstract_loopst::check_assertion(unsigned location,
                       std::inserter(diff, diff.begin()));
   // loops containing the update nodes should not be shrinkable
   for(auto loc: diff)
-  {
-    for(auto loop_n: insloop_map[loc])
-    {
-      irep_idt func = dep_graph[loc].PC->function;
-      abstract_loopt *loop_info = &(absloop_map[func].find(loop_n)->second);
-      loop_info->shrinkable = false;
-#ifdef DEBUG_ABSTRACT_LOOPS
-      std::cout << " - leaf node " << loc << " makes " << func << "::"
-        << loop_n << " unshrinkable\n";
-#endif
-    }
-  }
+    update_shrinkability(loc, dep_graph[loc].PC->function);
 
   // check dependence of update set
   diff.clear();
@@ -366,10 +363,17 @@ void abstract_loopst::check_assertion(unsigned location,
     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=
         dep_graph.reaching_definitions().get_value_sets();
       rw_range_set_value_sett rw_set(ns, value_sets);
-      goto_rw(dep_graph[loc].PC, rw_set);
+      rw_set.set_expr_r_set();
+      const code_assignt &code_assign = to_code_assign(inst.code);
+      rw_set.get_objects_rec(dep_graph[loc].PC,
+          rw_range_sett::get_modet::READ, code_assign.lhs());
       bool dep_on_loop_var = false;
       for(auto loop_n: insloop_map[loc])
       {
@@ -499,16 +503,16 @@ void abstract_loopst::get_loop_info(
   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;
-  }
+  //// 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