full instruction dispatch structure

Author: Remi Delmas

src/goto-instrument/contracts/dfcc.cpp

@@ -33,6 +33,7 @@ Author: Remi Delmas, [email protected]
 #include <ansi-c/cprover_library.h>
 // #include <goto-instrument/loop_utils.h>
 
+#include "instrument_spec_assigns.h"
 #include "utils.h"
 
 #include <iostream>
@@ -1209,7 +1210,15 @@ void dfcct::to_dfcc_checked_function(const irep_idt &function_id)
   log.debug() << "dfcc: to_dfcc_checked_function(" << function_id << ")"
               << messaget::eom;
 
-  // TODO fix problem with local_bitvector_analysis on library functions
+
+  // Create the cfg_info instance on a copy of the program before 
+  // instrumentation
+  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
+  goto_functiont goto_function_copy;
+  goto_function_copy.copy_from(goto_function);
+  const auto ns = namespacet(goto_model.symbol_table);
+  cfg_infot cfg_info(ns, goto_function_copy);
+
   const auto &function_symbol = get_function_symbol(function_id);
 
   // generate parameter symbols
@@ -1223,12 +1232,13 @@ void dfcct::to_dfcc_checked_function(const irep_idt &function_id)
 
   add_dfcc_params(dfcc_params, function_id);
 
-  instrument_function_body(function_id, dfcc_params);
+  instrument_function_body(function_id, dfcc_params, cfg_info);
 }
 
 void dfcct::instrument_function_body(
   const irep_idt &function_id,
-  const dfcc_parameter_symbolst &dfcc_params)
+  const dfcc_parameter_symbolst &dfcc_params,
+  cfg_infot cfg_info)
 {
   auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
 
@@ -1243,9 +1253,6 @@ void dfcct::instrument_function_body(
   auto &function_symbol = get_function_symbol(function_id);
   auto &body = goto_function.body;
 
-  // we might need to duplicate the goto_function to keep the analysis working
-  // as we modify the function body
-
   // add local declaration for __stack_allocated
   goto_programt preamble;
   preamble.add(goto_programt::make_decl(
@@ -1266,16 +1273,17 @@ void dfcct::instrument_function_body(
 
   body.destructive_insert(body.instructions.begin(), preamble);
 
-  // TODO add the DEAD instruction for stack_allocated at the end
+  // Insert `DEAD stack_allocated` before END_FUNCTION
   goto_programt::targett end_function = body.get_end_function();
   goto_programt::instructiont dead_inst = goto_programt::make_dead(
     dfcc_params.stack_allocated.symbol_expr(), function_symbol.location);
   body.insert_before_swap(end_function, dead_inst);
 
   const auto ns = namespacet(goto_model.symbol_table);
-  optionalt<cfg_infot> cfg_info_opt =
-    optionalt<cfg_infot>{cfg_infot{ns, goto_function}};
 
+  optionalt<cfg_infot> cfg_info_opt{cfg_info};
+
+  // instrument the whole body
   instrument_instructions(
     function_id,
     dfcc_params,
@@ -1319,6 +1327,7 @@ void dfcct::instrument_instructions(
   while(target != last_instruction) // excluding the last
   {
     // Skip instructions marked as disabled for assigns clause checking
+    // or rejected by the predicate
     if(
       // TODO
       // has_disable_assigns_check_pragma(target) ||
@@ -1331,53 +1340,234 @@ void dfcct::instrument_instructions(
     // Do not instrument this instruction again in the future,
     // since we are going to instrument it now below.
     // TODO
-    // add_pragma_disable_assigns_check(*target);
+    add_pragma_disable_assigns_check(*target);
 
-    if(
-      target->is_decl() &&
-      must_track_decl(target, cfg_info_opt))
+    if(target->is_decl() && must_track_decl_or_dead(target, cfg_info_opt))
+    {
+      instrument_decl(
+        function_id, dfcc_params, target, goto_program, cfg_info_opt);
+    }
+    if(target->is_dead() && must_track_decl_or_dead(target, cfg_info_opt))
     {
-      // // grab the declared symbol
-      // const auto &decl_symbol = target->decl_symbol();
-      // // move past the call and then insert the CAR
-      // target++;
-      // // since CAR was inserted *after* the DECL instruction,
-      // // move the instruction pointer backward,
-      // // because the enclosing while loop step takes
-      // // care of the increment
-      // target--;
+      instrument_dead(
+        function_id, dfcc_params, target, goto_program, cfg_info_opt);
     }
     else if(
       target->is_assign() &&
       must_check_assign(target, skip_function_params, cfg_info_opt))
     {
-      instrument_assign(target, goto_program, cfg_info_opt);
+      instrument_assign(
+        function_id, dfcc_params, target, goto_program, cfg_info_opt);
     }
     else if(target->is_function_call())
     {
-      instrument_fuction_call(target, goto_program, cfg_info_opt);
+      instrument_function_call(
+        function_id, dfcc_params, target, goto_program, cfg_info_opt);
     }
-    else if(
-      target->is_dead() &&
-      must_track_dead(target, cfg_info_opt))
+    else if(target->is_other())
     {
-      // const auto &symbol = target->dead_symbol();
-      // // TODO
+      instrument_other(
+        function_id, dfcc_params, target, goto_program, cfg_info_opt);
     }
-    else if(
-      target->is_other() &&
-      target->get_other().get_statement() == ID_havoc_object)
+    // else do nothing
+    target++;
+  }
+}
+
+bool dfcct::must_track_decl_or_dead(
+  const goto_programt::targett &target,
+  const optionalt<cfg_infot> &cfg_info_opt) const
+{
+  INVARIANT(
+    target->is_decl() || target->is_dead(),
+    "the target must be a DECL or DEAD instruction");
+
+  const auto &ident = target->is_decl()
+                        ? target->decl_symbol().get_identifier()
+                        : target->dead_symbol().get_identifier();
+  return !cfg_info_opt.has_value() ||
+         (cfg_info_opt.has_value() &&
+          cfg_info_opt.value().is_not_local_or_dirty_local(ident));
+}
+
+void dfcct::instrument_decl(
+  const irep_idt &function_id,
+  const dfcc_parameter_symbolst &dfcc_params,
+  goto_programt::targett &target,
+  goto_programt &goto_program,
+  optionalt<cfg_infot> &cfg_info_opt)
+{
+  // // grab the declared symbol
+  // const auto &decl_symbol = target->decl_symbol();
+  // // move past the call and then insert the CAR
+  // target++;
+  // // since CAR was inserted *after* the DECL instruction,
+  // // move the instruction pointer backward,
+  // // because the enclosing while loop step takes
+  // // care of the increment
+  // target--;
+}
+
+void dfcct::instrument_dead(
+  const irep_idt &function_id,
+  const dfcc_parameter_symbolst &dfcc_params,
+  goto_programt::targett &target,
+  goto_programt &goto_program,
+  optionalt<cfg_infot> &cfg_info_opt)
+{
+}
+
+/// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented.
+bool dfcct::must_check_assign(
+  const goto_programt::const_targett &target,
+  dfcc_skip_function_paramst skip_function_params,
+  const optionalt<cfg_infot> &cfg_info_opt)
+{
+  log.debug().source_location = target->source_location();
+
+  if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
+  {
+    const auto &symbol_expr = to_symbol_expr(target->assign_lhs());
+    if(
+      skip_function_params == dfcc_skip_function_paramst::NO &&
+      goto_model.symbol_table.lookup_ref(symbol_expr.get_identifier())
+        .is_parameter)
     {
-      // // TODO array copy and the rest
-      // auto havoc_argument = target->get_other().operands().front();
-      // auto havoc_object = pointer_object(havoc_argument);
+      log.debug() << "dfcc: checking assignment to function parameter "
+                  << format(symbol_expr) << messaget::eom;
+      return true;
     }
 
-    // Move to the next instruction
-    target++;
+    if(cfg_info_opt.has_value())
+    {
+      if(cfg_info_opt.value().is_local(symbol_expr.get_identifier()))
+      {
+        log.debug() << "dfcc: skipping checking on assignment to local symbol "
+                    << format(symbol_expr) << messaget::eom;
+        return false;
+      }
+      else
+      {
+        log.debug() << "dfcc: checking assignment to non-local symbol "
+                    << format(symbol_expr) << messaget::eom;
+        return true;
+      }
+    }
+    log.debug() << "dfcc: checking assignment to symbol " << format(symbol_expr)
+                << messaget::eom;
+    return true;
   }
+  else
+  {
+    // This is not a mere symbol.
+    // Since non-dirty locals are not tracked explicitly in the write set,
+    // we need to skip the check if we can verify that the expression describes
+    // an access to a non-dirty local symbol or an input parameter,
+    // otherwise the check will fail.
+    // In addition, the expression shall not contain address_of or dereference
+    // operators, regardless of the base symbol/object on which they apply.
+    // If the expression contains an address_of operation, the assignment gets
+    // checked. If the base object is a local or a parameter, it will also be
+    // flagged as dirty and will be tracked explicitly, and the check will pass.
+    // If the expression contains a dereference operation, the assignment gets
+    // checked. If the dereferenced address was computed from a local object,
+    // from a function parameter or returned by a local malloc,
+    // then the object will be tracked explicitly and the check will pass.
+    // In all other cases (address of a non-local object, or dereference of
+    // a non-locally computed address) the location must be given explicitly
+    // in the assigns clause to be tracked and we must check the assignment.
+    if(
+      cfg_info_opt.has_value() &&
+      cfg_info_opt.value().is_local_composite_access(target->assign_lhs()))
+    {
+      log.debug() << "dfcc: skipping check on assignment to local composite "
+                     "member expression "
+                  << format(target->assign_lhs()) << messaget::eom;
+      return false;
+    }
+    log.debug() << "dfcc: checking assignment to expression "
+                << format(target->assign_lhs()) << messaget::eom;
+    return true;
+  }
+}
+
+void dfcct::instrument_assign(
+  const irep_idt &function_id,
+  const dfcc_parameter_symbolst &dfcc_params,
+  goto_programt::targett &target,
+  goto_programt &goto_program,
+  optionalt<cfg_infot> &cfg_info_opt)
+{
 }
 
+void dfcct::instrument_function_call(
+  const irep_idt &function_id,
+  const dfcc_parameter_symbolst &dfcc_params,
+  goto_programt::targett &target,
+  goto_programt &goto_program,
+  optionalt<cfg_infot> &cfg_info_opt)
+{
+  INVARIANT(
+    target->is_function_call(),
+    "the target must be a function call instruction");
+
+  // do we have a function symbol or a complex expression ?
+  const auto &callee_expr = target->call_function();
+  if(callee_expr.id() == ID_symbol)
+  {
+    // we have a function symbol
+    const auto &callee_id =
+      id2string(to_symbol_expr(callee_expr).get_identifier());
+
+    if(callee_id == CPROVER_PREFIX "allocate")
+    {
+      // heap allocation
+    }
+    else if(callee_id == CPROVER_PREFIX "deallocate")
+    {
+      // heap deallocation
+    }
+    else if(callee_id == "__builtin_alloca")
+    {
+      // dynamic stack allocation
+    }
+    else
+    {
+      // user defined or library function
+      // propagate dfcc parameters
+    }
+  }
+  else
+  {
+    // we have a function pointer expression
+    // propagate the dfcc params
+  }
+}
+
+void dfcct::instrument_other(
+  const irep_idt &function_id,
+  const dfcc_parameter_symbolst &dfcc_params,
+  goto_programt::targett &target,
+  goto_programt &goto_program,
+  optionalt<cfg_infot> &cfg_info_opt)
+{
+  auto &statement = target->get_other().get_statement();
+  if(statement == ID_array_set)
+  {
+  }
+  else if(statement == ID_array_copy)
+  {
+  }
+  else if(statement == ID_array_replace)
+  {
+  }
+  else if(statement == ID_havoc_object)
+  {
+  }
+  else
+  {
+  }
+}
 
 const symbolt &dfcct::clone_and_rename_function(
   const irep_idt &function_id,