instrumentation for preconditions

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/convert_nondet.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
@@ -780,6 +781,9 @@ bool cbmc_parse_optionst::process_goto_program(
 
     mm_io(goto_model);
 
+    // instrument library preconditions
+    instrument_preconditions(goto_model);
+
     // do partial inlining
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_model, get_message_handler());

src/goto-programs/Makefile

@@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \
       goto_program_template.cpp \
       goto_trace.cpp \
       graphml_witness.cpp \
+      instrument_preconditions.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \

src/goto-programs/instrument_preconditions.cpp

@@ -0,0 +1,148 @@
+/*******************************************************************\
+
+Module: Move preconditions of a function
+        to the call-site of the function
+
+Author: Daniel Kroening
+
+Date:   September 2017
+
+\*******************************************************************/
+
+#include "instrument_preconditions.h"
+
+#include <util/replace_symbol.h>
+
+std::vector<goto_programt::const_targett> get_preconditions(
+  const symbol_exprt &function,
+  const goto_functionst &goto_functions)
+{
+  const irep_idt &identifier=function.get_identifier();
+
+  auto f_it=goto_functions.function_map.find(identifier);
+  if(f_it==goto_functions.function_map.end())
+    return {};
+
+  const auto &body=f_it->second.body;
+
+  std::vector<goto_programt::const_targett> result;
+
+  for(auto i_it=body.instructions.begin();
+      i_it!=body.instructions.end();
+      i_it++)
+  {
+    if(i_it->is_location() ||
+       i_it->is_skip())
+      continue; // ignore
+
+    if(i_it->is_assert() &&
+       i_it->source_location.get_property_class()==ID_precondition)
+      result.push_back(i_it);
+    else
+      break; // preconditions must be at the front
+  }
+
+  return result;
+}
+
+void remove_preconditions(goto_programt &goto_program)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_location() ||
+       instruction.is_skip())
+      continue; // ignore
+
+    if(instruction.is_assert() &&
+       instruction.source_location.get_property_class()==ID_precondition)
+      instruction.type=LOCATION;
+    else
+      break; // preconditions must be at the front
+  }
+}
+
+replace_symbolt actuals_replace_map(
+  const code_function_callt &call,
+  const namespacet &ns)
+{
+  PRECONDITION(call.function().id()==ID_symbol);
+  const symbolt &s=ns.lookup(to_symbol_expr(call.function()));
+  const auto &code_type=to_code_type(s.type);
+  const auto &parameters=code_type.parameters();
+  const auto &arguments=call.arguments();
+
+  replace_symbolt result;
+  std::size_t count=0;
+  for(const auto &p : parameters)
+  {
+    if(p.get_identifier()!=irep_idt() &&
+       arguments.size()>count)
+    {
+      exprt a=arguments[count];
+      if(a.type()!=p.type())
+        a=typecast_exprt(a, p.type());
+      symbol_exprt s(p.get_identifier(), p.type());
+      result.insert(s, a);
+    }
+    count++;
+  }
+
+  return result;
+}
+
+void instrument_preconditions(
+  const goto_modelt &goto_model,
+  goto_programt &goto_program)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  for(auto it=goto_program.instructions.begin();
+      it!=goto_program.instructions.end();
+      it++)
+  {
+    if(it->is_function_call())
+    {
+      // does the function we call have preconditions?
+      const auto &call=to_code_function_call(it->code);
+
+      if(call.function().id()==ID_symbol)
+      {
+        auto preconditions=
+          get_preconditions(to_symbol_expr(call.function()),
+                            goto_model.goto_functions);
+
+        source_locationt source_location=it->source_location;
+        irep_idt function=it->function;
+
+        replace_symbolt r=actuals_replace_map(call, ns);
+
+        // add before the call, with location of the call
+        for(const auto &p : preconditions)
+        {
+          goto_program.insert_before_swap(it);
+          exprt instance=p->guard;
+          r(instance);
+          it->make_assertion(instance);
+          it->function=function;
+          it->source_location=source_location;
+          it->source_location.set_property_class(ID_precondition_instance);
+          it->source_location.set_comment(p->source_location.get_comment());
+          it++;
+        }
+      }
+    }
+  }
+}
+
+void instrument_preconditions(goto_modelt &goto_model)
+{
+  // add at call site
+  for(auto &f_it : goto_model.goto_functions.function_map)
+    instrument_preconditions(
+      goto_model,
+      f_it.second.body);
+
+  // now remove the preconditions
+  for(auto &f_it : goto_model.goto_functions.function_map)
+    remove_preconditions(f_it.second.body);
+}

src/goto-programs/instrument_preconditions.h

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Move preconditions of a function
+        to the call-site of the function
+
+Author: Daniel Kroening
+
+Date:   September 2017
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
+#define CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
+
+#include <goto-programs/goto_model.h>
+
+void instrument_preconditions(goto_modelt &);
+
+#endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H

src/util/irep_ids.def

@@ -91,6 +91,7 @@ IREP_ID_ONE(assume)
 IREP_ID_ONE(assert)
 IREP_ID_ONE(assertion)
 IREP_ID_ONE(precondition)
+IREP_ID_ONE(precondition_instance)
 IREP_ID_ONE(goto)
 IREP_ID_ONE(gcc_computed_goto)
 IREP_ID_ONE(ifthenelse)