Added flags to goto-diff

minor bug fixing, compact output mode for the demo, forward and backward
only impact

Author: AnnaTrost

src/goto-diff/change_impact.cpp

@@ -239,11 +239,16 @@ class change_impactt
 public:
   change_impactt(
     const goto_modelt &model_old,
-    const goto_modelt &model_new);
+    const goto_modelt &model_new,
+    impact_modet impact_mode,
+    bool compact_output);
 
   void operator()();
 
 protected:
+  impact_modet impact_mode;
+  bool compact_output;
+
   const goto_functionst &old_goto_functions;
   const namespacet ns_old;
   const goto_functionst &new_goto_functions;
@@ -301,6 +306,12 @@ class change_impactt
     const goto_program_change_impactt &n_c_i,
     const goto_functionst &n_goto_functions,
     const namespacet &n_ns) const;
+
+  void output_instruction(char prefix,
+      const goto_programt &goto_program,
+      const namespacet &ns,
+      const irep_idt &function,
+      goto_programt::const_targett& target) const;
 };
 
 /*******************************************************************\
@@ -317,7 +328,11 @@ Function: change_impactt::change_impactt
 
 change_impactt::change_impactt(
     const goto_modelt &model_old,
-    const goto_modelt &model_new):
+    const goto_modelt &model_new,
+    impact_modet _impact_mode,
+    bool _compact_output):
+  impact_mode(_impact_mode),
+  compact_output(_compact_output),
   old_goto_functions(model_old.goto_functions),
   ns_old(model_old.symbol_table),
   new_goto_functions(model_new.goto_functions),
@@ -425,8 +440,10 @@ void change_impactt::change_impact(
           const dependence_grapht::nodet &d_node=
             old_dep_graph[old_dep_graph[o_it].get_node_id()];
 
-          propogate_dep_back(d_node, old_dep_graph, old_change_impact, true);
-          propogate_dep_forward(d_node, old_dep_graph, old_change_impact, true);
+          if(impact_mode == BACKWARD || impact_mode == BOTH)
+            propogate_dep_back(d_node, old_dep_graph, old_change_impact, true);
+          if(impact_mode == FORWARD || impact_mode == BOTH)
+            propogate_dep_forward(d_node, old_dep_graph, old_change_impact, true);
         }
         old_impact[o_it]|=DELETED;
         ++o_it;
@@ -438,8 +455,10 @@ void change_impactt::change_impact(
           const dependence_grapht::nodet &d_node=
             new_dep_graph[new_dep_graph[n_it].get_node_id()];
 
-          propogate_dep_back(d_node, new_dep_graph, new_change_impact, false);
-          propogate_dep_forward(d_node, new_dep_graph, new_change_impact, false);
+          if(impact_mode == BACKWARD || impact_mode == BOTH)
+            propogate_dep_back(d_node, new_dep_graph, new_change_impact, false);
+          if(impact_mode == FORWARD || impact_mode == BOTH)
+            propogate_dep_forward(d_node, new_dep_graph, new_change_impact, false);
         }
         new_impact[n_it]|=NEW;
         ++n_it;
@@ -464,26 +483,25 @@ Function: change_impactt::propogate_dep_forward
 void change_impactt::propogate_dep_forward(const dependence_grapht::nodet &d_node,
 		const dependence_grapht &dep_graph,
 		goto_functions_change_impactt &change_impact, bool del) {
-	for (dependence_grapht::edgest::const_iterator it = d_node.out.begin();
-			it != d_node.out.end(); ++it) {
-		goto_programt::const_targett src = dep_graph[it->first].PC;
-
-		mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
-		mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
-
-			if ((change_impact[src->function][src] & data_flag)
-					|| (change_impact[src->function][src] & ctrl_flag))
-				continue;
-			if (it->second.get() == dep_edget::DATA
-					|| it->second.get() == dep_edget::BOTH)
-				change_impact[src->function][src] |= data_flag;
-			else
-				change_impact[src->function][src] |= ctrl_flag;
-			propogate_dep_forward(
-					dep_graph[dep_graph[src].get_node_id()], dep_graph,
-					change_impact, del);
-	}
+  for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
+      it != d_node.out.end(); ++it)
+  {
+    goto_programt::const_targett src = dep_graph[it->first].PC;
 
+    mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
+    mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
+
+    if((change_impact[src->function][src] & data_flag)
+        || (change_impact[src->function][src] & ctrl_flag))
+      continue;
+    if(it->second.get() == dep_edget::DATA
+        || it->second.get() == dep_edget::BOTH)
+      change_impact[src->function][src] |= data_flag;
+    else
+      change_impact[src->function][src] |= ctrl_flag;
+    propogate_dep_forward(dep_graph[dep_graph[src].get_node_id()], dep_graph,
+        change_impact, del);
+  }
 }
 
 /*******************************************************************\
@@ -501,27 +519,28 @@ Function: change_impactt::propogate_dep_back
 void change_impactt::propogate_dep_back(const dependence_grapht::nodet &d_node,
 		const dependence_grapht &dep_graph,
 		goto_functions_change_impactt &change_impact, bool del) {
-	for (dependence_grapht::edgest::const_iterator it = d_node.in.begin();
-			it != d_node.in.end(); ++it) {
-		goto_programt::const_targett src = dep_graph[it->first].PC;
-
-		mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
-		mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
-
-		if ((change_impact[src->function][src] & data_flag)
-				|| (change_impact[src->function][src] & ctrl_flag)) {
-			continue;
-		}
-		if (it->second.get() == dep_edget::DATA
-				|| it->second.get() == dep_edget::BOTH)
-			change_impact[src->function][src] |= data_flag;
-		else
-			change_impact[src->function][src] |= ctrl_flag;
-
-		propogate_dep_back(
-				dep_graph[dep_graph[src].get_node_id()], dep_graph,
-				change_impact, del);
-	}
+  for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
+      it != d_node.in.end(); ++it)
+  {
+    goto_programt::const_targett src = dep_graph[it->first].PC;
+
+    mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
+    mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
+
+    if((change_impact[src->function][src] & data_flag)
+        || (change_impact[src->function][src] & ctrl_flag))
+    {
+      continue;
+    }
+    if(it->second.get() == dep_edget::DATA
+        || it->second.get() == dep_edget::BOTH)
+      change_impact[src->function][src] |= data_flag;
+    else
+      change_impact[src->function][src] |= ctrl_flag;
+
+    propogate_dep_back(dep_graph[dep_graph[src].get_node_id()], dep_graph,
+        change_impact, del);
+  }
 }
 
 /*******************************************************************\
@@ -629,7 +648,8 @@ void change_impactt::output_change_impact(
   assert(f_it!=goto_functions.function_map.end());
   const goto_programt &goto_program=f_it->second.body;
 
-  std::cout << "/** " << function << " **/\n";
+  if(!compact_output)
+    std::cout << "/** " << function << " **/\n";
 
   forall_goto_program_instructions(target, goto_program)
   {
@@ -658,8 +678,7 @@ void change_impactt::output_change_impact(
     else
       assert(false);
 
-    std::cout << prefix;
-    goto_program.output_instruction(ns, function, std::cout, target);
+    output_instruction(prefix, goto_program, ns, function, target);
   }
 }
 
@@ -694,7 +713,8 @@ void change_impactt::output_change_impact(
   assert(f_it!=n_goto_functions.function_map.end());
   const goto_programt &goto_program=f_it->second.body;
 
-  std::cout << "/** " << function << " **/\n";
+  if(!compact_output)
+    std::cout << "/** " << function << " **/\n";
 
   goto_programt::const_targett o_target=
     old_goto_program.instructions.begin();
@@ -707,14 +727,9 @@ void change_impactt::output_change_impact(
 
     if(old_mod_flags&DELETED)
     {
-      std::cout << '-';
-      goto_program.output_instruction(
-        o_ns,
-        function,
-        std::cout,
-        o_target);
-
+      output_instruction('-', goto_program, o_ns, function, o_target);
       ++o_target;
+      --target;
       continue;
     }
 
@@ -764,8 +779,7 @@ void change_impactt::output_change_impact(
     else
       assert(false);
 
-    std::cout << prefix;
-    goto_program.output_instruction(n_ns, function, std::cout, target);
+    output_instruction(prefix, goto_program, n_ns, function, target);
   }
   for( ;
       o_target!=old_goto_program.instructions.end();
@@ -792,8 +806,41 @@ void change_impactt::output_change_impact(
     else
       assert(false);
 
+    output_instruction(prefix, goto_program, o_ns, function, o_target);
+  }
+}
+
+/*******************************************************************\
+
+Function: change_impactt::output_instruction
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void change_impactt::output_instruction(char prefix,
+    const goto_programt &goto_program,
+    const namespacet &ns,
+    const irep_idt &function,
+    goto_programt::const_targett& target) const
+{
+  if(compact_output)
+  {
+    if(prefix == ' ')
+      return;
+    const irep_idt &file=target->source_location.get_file();
+    const irep_idt &line=target->source_location.get_line();
+    if (!file.empty() && !line.empty())
+      std::cout << prefix << " " << id2string(file)
+          << " " << id2string(line) << std::endl;
+  } else
+  {
     std::cout << prefix;
-    goto_program.output_instruction(o_ns, function, std::cout, o_target);
+    goto_program.output_instruction(ns, function, std::cout, target);
   }
 }
 
@@ -811,8 +858,10 @@ Function: change_impact
 
 void change_impact(
   const goto_modelt &model_old,
-  const goto_modelt &model_new)
+  const goto_modelt &model_new,
+  impact_modet impact_mode,
+  bool compact_output)
 {
-  change_impactt c(model_old, model_new);
+  change_impactt c(model_old, model_new, impact_mode, compact_output);
   c();
 }

src/goto-diff/change_impact.h

@@ -12,9 +12,12 @@ Date: April 2016
 #define CPROVER_CHANGE_IMPACT_H
 
 class goto_modelt;
+typedef enum {FORWARD, BACKWARD, BOTH} impact_modet;
 
 void change_impact(
   const goto_modelt &model_old,
-  const goto_modelt &model_new);
+  const goto_modelt &model_new,
+  impact_modet impact_mode,
+  bool compact_output);
 
 #endif

src/goto-diff/goto_diff_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Peter Schrammel
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_returns.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -330,14 +331,24 @@ int goto_diff_parse_optionst::doit()
     namespacet ns1(goto_model1.symbol_table);
     goto_model1.goto_functions.output(ns1, std::cout);
     std::cout << "*******************************************************\n";
-    namespacet ns2(goto_model1.symbol_table);
+    namespacet ns2(goto_model2.symbol_table);
     goto_model2.goto_functions.output(ns2, std::cout);
     return 0;
   }
 
-  if(cmdline.isset("change-impact"))
+  if(cmdline.isset("change-impact") ||
+     cmdline.isset("forward-impact")||
+	 cmdline.isset("backward-impact"))
   {
-    change_impact(goto_model1, goto_model2);
+    //Workaround to avoid deps not propagating between return and end_func
+    remove_returns(goto_model1);
+    remove_returns(goto_model2);
+
+    impact_modet impact_mode =
+        cmdline.isset("forward-impact") ?
+            FORWARD : (cmdline.isset("backward-impact") ? BACKWARD : BOTH);
+    change_impact(goto_model1, goto_model2, impact_mode,
+          cmdline.isset("compact-output"));
     return 0;
   }
 
@@ -536,7 +547,10 @@ void goto_diff_parse_optionst::help()
     " --show-functions             show functions (default)\n"
     " --syntactic                  do syntactic diff (default)\n"
     " -u | --unified               output unified diff\n"
-    " --change-impact              output unified diff with dependencies\n"
+    " --change-impact | \n"
+    "  --forward-impact |\n"
+    "  --backward-impact           output unified diff with forward&backward/forward/backward dependencies\n"
+    " --compact-output             output dependencies in compact mode\n"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

src/goto-diff/goto_diff_parse_options.h

@@ -23,7 +23,8 @@ class optionst;
   "(json-ui)" \
   "(show-goto-functions)" \
   "(verbosity):(version)" \
-  "u(unified)(change-impact)"
+  "u(unified)(change-impact)(forward-impact)(backward-impact)" \
+  "(compact-output)"
 
 class goto_diff_parse_optionst:
   public parse_options_baset,