Adds --expand-pointer-predicates to goto-instrument [depends-on: #3769, blocks #2706]

src/ansi-c/c_typecheck_expr.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -32,6 +33,8 @@ Author: Daniel Kroening, [email protected]
 #include "anonymous_member.h"
 #include "padding.h"
 
+bool is_lvalue(const exprt &expr);
+
 void c_typecheck_baset::typecheck_expr(exprt &expr)
 {
   if(expr.id()==ID_already_typechecked)
@@ -2085,6 +2088,47 @@ exprt c_typecheck_baset::do_special_functions(
 
     return same_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "points_to_valid_memory")
+  {
+    if(expr.arguments().size()!=2)
+    {
+      err_location(f_op);
+      error() << "points_to_valid_memory expects two operands" << eom;
+      throw 0;
+    }
+    if(!is_lvalue(expr.arguments().front()))
+    {
+      err_location(f_op);
+      error() << "ptr argument to points_to_valid_memory"
+              << " must be an lvalue" << eom;
+      throw 0;
+    }
+
+    exprt same_object_expr;
+    if(expr.arguments().size() == 2)
+    {
+      // TODO: We should add some way to enforce that the second argument
+      // has a reasonable type (coercible to __CPROVER_size_t).
+#if 0
+      if(expr.arguments()[1].type() <[cannot be coerced to size_t]>)
+      {
+        err_location(f_op);
+        error() << "size argument to points_to_valid_memory"
+                << " must be coercible to size_t" << eom;
+        throw 0;
+      }
+#endif
+      same_object_expr =
+        points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]);
+    }
+    else
+    {
+      UNREACHABLE;
+    }
+    same_object_expr.add_source_location()=source_location;
+
+    return same_object_expr;
+  }
   else if(identifier==CPROVER_PREFIX "buffer_size")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -6,6 +6,7 @@ void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_invalid_pointer(const void *);
+__CPROVER_bool __CPROVER_points_to_valid_memory(const void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);

src/ansi-c/expr2c.cpp

@@ -3521,6 +3521,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_good_pointer)
     return convert_function(src, "GOOD_POINTER", precedence=16);
 
+  else if(src.id()==ID_points_to_valid_memory)
+    return convert_function(src, "POINTS_TO_VALID_MEMORY", precedence=16);
+
   else if(src.id()==ID_object_size)
     return convert_function(src, "OBJECT_SIZE", precedence=16);
 

src/goto-instrument/Makefile

@@ -32,6 +32,7 @@ SRC = accelerate/accelerate.cpp \
       document_properties.cpp \
       dot.cpp \
       dump_c.cpp \
+      expand_pointer_predicates.cpp \
       full_slicer.cpp \
       function.cpp \
       function_modifies.cpp \

src/goto-instrument/expand_pointer_predicates.cpp

@@ -0,0 +1,220 @@
+/*******************************************************************\
+
+Module: Expand pointer predicates in assertions/assumptions.
+
+Author: Klaas Pruiksma
+
+Date: June 2018
+
+\*******************************************************************/
+
+/// \file
+/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory)
+/// in assumptions and assertions with suitable expressions and additional
+/// instructions.
+
+#include "expand_pointer_predicates.h"
+
+#include <analyses/local_bitvector_analysis.h>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/expr_iterator.h>
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
+#include <util/namespace.h>
+#include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+
+#include <goto-programs/goto_model.h>
+
+class expand_pointer_predicatest
+{
+public:
+  expand_pointer_predicatest(
+    symbol_tablet &_symbol_table,
+    goto_functionst &_goto_functions):
+      ns(_symbol_table),
+      symbol_table(_symbol_table),
+      goto_functions(_goto_functions),
+      local_bitvector_analysis(nullptr)
+  {
+  }
+
+  void operator()();
+
+protected:
+  namespacet ns;
+  symbol_tablet &symbol_table;
+  goto_functionst &goto_functions;
+  local_bitvector_analysist *local_bitvector_analysis;
+
+  void expand_pointer_predicates();
+
+  void expand_assumption(
+    goto_programt &program,
+    goto_programt::targett target,
+    exprt &assume_expr);
+
+  void expand_assertion(exprt &assert_expr);
+
+  const symbolt &new_tmp_symbol(
+    const typet &type,
+    const source_locationt &source_location);
+};
+
+bool is_lvalue(const exprt &expr);
+
+void expand_pointer_predicatest::expand_pointer_predicates()
+{
+  Forall_goto_functions(f_it, goto_functions)
+  {
+    goto_functionst::goto_functiont &goto_function = f_it->second;
+    local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
+    local_bitvector_analysis = &local_bitvector_analysis_obj;
+    Forall_goto_program_instructions(i_it, goto_function.body)
+    {
+      if(i_it->is_assert())
+      {
+        expand_assertion(i_it->guard);
+      }
+      else if(i_it->is_assume())
+      {
+        expand_assumption(
+          goto_function.body,
+          i_it,
+          i_it->guard);
+          local_bitvector_analysis_obj =
+            local_bitvector_analysist(goto_function);
+          local_bitvector_analysis = &local_bitvector_analysis_obj;
+      }
+      else
+      {
+        continue;
+      }
+    }
+  }
+}
+
+void expand_pointer_predicatest::expand_assumption(
+  goto_programt &program,
+  goto_programt::targett target,
+  exprt &assume_expr)
+{
+  goto_programt assume_code;
+  for(depth_iteratort it=assume_expr.depth_begin();
+      it != assume_expr.depth_end();)
+  {
+    if(it->id() == ID_points_to_valid_memory)
+    {
+      exprt &valid_memory_expr = it.mutate();
+      exprt &pointer_expr = valid_memory_expr.op0();
+      exprt size_expr = valid_memory_expr.op1();
+      simplify(size_expr, ns);
+
+      // This should be forced by typechecking.
+      INVARIANT(pointer_expr.type().id() == ID_pointer &&
+                  is_lvalue(pointer_expr),
+                "Invalid argument to valid_pointer.");
+
+      local_bitvector_analysist::flagst flags =
+        local_bitvector_analysis->get(target, pointer_expr);
+      // Only create a new object if the pointer may be uninitialized.
+      if(flags.is_uninitialized() || flags.is_unknown())
+      {
+        typet object_type = type_from_size(size_expr, ns);
+
+        // Decl a new variable (which is therefore unconstrained)
+        goto_programt::targett d = assume_code.add_instruction(DECL);
+        d->function = target->function;
+        d->source_location = assume_expr.source_location();
+        const symbol_exprt obj =
+          new_tmp_symbol(object_type, d->source_location).symbol_expr();
+        d->code=code_declt(obj);
+
+        exprt rhs;
+        if(object_type.id() == ID_array)
+        {
+          rhs = typecast_exprt(
+            address_of_exprt(
+              index_exprt(obj, from_integer(0, index_type()))),
+            pointer_expr.type());
+        }
+        else
+        {
+          rhs = address_of_exprt(obj);
+        }
+
+        // Point the relevant pointer to the new object
+        goto_programt::targett a = assume_code.add_instruction(ASSIGN);
+        a->function = target->function;
+        a->source_location = assume_expr.source_location();
+        a->code = code_assignt(pointer_expr, rhs);
+        a->code.add_source_location() = assume_expr.source_location();
+      }
+
+      // Because some uses of this occur before deallocated, dead, and malloc
+      // objects are initialized, we need to make some additional assumptions
+      // to clarify that our newly allocated object is not dead, deallocated,
+      // or outside the bounds of a malloc region.
+
+      exprt check_expr =
+        points_to_valid_memory_def(pointer_expr, size_expr, ns);
+      valid_memory_expr.swap(check_expr);
+      it.next_sibling_or_parent();
+    }
+    else {
+      ++it;
+    }
+  }
+
+  program.destructive_insert(target, assume_code);
+}
+
+void expand_pointer_predicatest::expand_assertion(exprt &assert_expr)
+{
+  for(depth_iteratort it = assert_expr.depth_begin();
+      it != assert_expr.depth_end();)
+  {
+    if(it->id() == ID_points_to_valid_memory)
+    {
+      // Build an expression that checks validity.
+      exprt &valid_memory_expr = it.mutate();
+      exprt &pointer_expr = valid_memory_expr.op0();
+      exprt &size_expr = valid_memory_expr.op1();
+
+      exprt check_expr =
+        points_to_valid_memory_def(pointer_expr, size_expr, ns);
+      valid_memory_expr.swap(check_expr);
+      it.next_sibling_or_parent();
+    }
+    else
+    {
+      ++it;
+    }
+  }
+}
+
+const symbolt &expand_pointer_predicatest::new_tmp_symbol(
+  const typet &type,
+  const source_locationt &source_location)
+{
+  return get_fresh_aux_symbol(
+    type,
+    id2string(source_location.get_function()),
+    "tmp_epp",
+    source_location,
+    ID_C,
+    symbol_table);
+}
+
+void expand_pointer_predicatest::operator()()
+{
+  expand_pointer_predicates();
+}
+
+void expand_pointer_predicates(goto_modelt &goto_model)
+{
+  expand_pointer_predicatest(goto_model.symbol_table,
+                             goto_model.goto_functions)();
+}

src/goto-instrument/expand_pointer_predicates.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Expand pointer predicates in assertions/assumptions.
+
+Author: Klaas Pruiksma
+
+Date: June 2018
+
+\*******************************************************************/
+
+/// \file
+/// Replace pointer predicates (e.g. __CPROVER_points_to_valid_memory)
+/// in assumptions and assertions with suitable expressions and additional
+/// instructions.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H
+#define CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H
+
+class goto_modelt;
+
+void expand_pointer_predicates(goto_modelt &goto_model);
+
+#endif // CPROVER_GOTO_INSTRUMENT_EXPAND_POINTER_PREDICATES_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -76,6 +76,7 @@ Author: Daniel Kroening, [email protected]
 #include "document_properties.h"
 #include "dot.h"
 #include "dump_c.h"
+#include "expand_pointer_predicates.h"
 #include "full_slicer.h"
 #include "function.h"
 #include "havoc_loops.h"
@@ -1053,6 +1054,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     code_contracts(goto_model);
   }
 
+  if(cmdline.isset("expand-pointer-predicates"))
+  {
+    expand_pointer_predicates(goto_model);
+  }
+
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
   {
@@ -1622,6 +1628,7 @@ void goto_instrument_parse_optionst::help()
     " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
+    " --expand-pointer-predicates  Expands predicates about pointers (e.g. __CPROVER_points_to_valid_memory) into a form useable by CBMC\n" // NOLINT(*)
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
     " --add-library                add models of C library functions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -88,6 +88,7 @@ Author: Daniel Kroening, [email protected]
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
+  "(expand-pointer-predicates)" \
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\