Insert final assert false pass

regression/goto-instrument/insert-final-assert-false1/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+int main()
+{
+  size_t n;
+  int *p = (int *)malloc(n);
+  int *q = (int *)malloc(n);
+  __CPROVER_assert(p, "not-null");
+  __CPROVER_assert(q, "not-null");
+  // the following is the same as assuming false
+  __CPROVER_assume(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT(q));
+  return 0;
+}

regression/goto-instrument/insert-final-assert-false1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--insert-final-assert-false main
+^EXIT=0$
+^SIGNAL=0$
+insert-final-assert-false \(should fail\) : SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test has a false assumption meaning the program passes vacuously. A sign
+that this is the case is that verification succeeds with a false assert inserted
+automatically by the --insert-final-assert-false flag.

regression/goto-instrument/insert-final-assert-false2/main.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int main()
+{
+  size_t n;
+  int *p = (int *)malloc(n);
+  int *q = (int *)malloc(n);
+  __CPROVER_assert(p, "not-null");
+  __CPROVER_assert(q, "not-null");
+  return 0;
+}

regression/goto-instrument/insert-final-assert-false2/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--insert-final-assert-false main
+^EXIT=10$
+^SIGNAL=0$
+insert-final-assert-false \(should fail\) : FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test does not have a false assumption. A sign that this is the case is
+that verification fails with a false assert inserted automatically by the
+--insert-final-assert-false flag.

regression/goto-instrument/insert-final-assert-false3/main.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int nondet_int();
+int main()
+{
+  if(nondet_int())
+  {
+    return 0;
+  }
+  else
+  {
+    return 1;
+  }
+}

regression/goto-instrument/insert-final-assert-false3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--insert-final-assert-false main
+^EXIT=10$
+^SIGNAL=0$
+insert-final-assert-false \(should fail\) : FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test does not have a false assumption (and has multiple return paths). A
+sign that this is the case is that verification fails with a false assert
+inserted automatically by the --insert-final-assert-false flag.

regression/goto-instrument/insert-final-assert-false4/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+int nondet_int();
+int main()
+{
+  if(nondet_int())
+  {
+    __CPROVER_assume(0 == 1);
+    return 0;
+  }
+  else
+  {
+    return 1;
+  }
+}

regression/goto-instrument/insert-final-assert-false4/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--insert-final-assert-false main
+^EXIT=10$
+^SIGNAL=0$
+insert-final-assert-false \(should fail\) : FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test has a false assumption on one of its return paths (but not both).
+This shows a limitation of the --insert-final-assert-false pass since the
+verification still fails with the inserted assert.

regression/goto-instrument/insert-final-assert-false5/main.c

@@ -0,0 +1,6 @@
+#include <stdlib.h>
+
+int main()
+{
+  return 0;
+}

regression/goto-instrument/insert-final-assert-false5/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--insert-final-assert-false function_that_does_not_exist
+^EXIT=6$
+^SIGNAL=0$
+insert-final-assert-false: could not find function
+--
+--
+This test tries to use --insert-final-assert-false on a function that does not
+exist in the program.

src/goto-instrument/Makefile

@@ -42,6 +42,7 @@ SRC = accelerate/accelerate.cpp \
       goto_program2code.cpp \
       havoc_loops.cpp \
       horn_encoding.cpp \
+      insert_final_assert_false.cpp \
       interrupt.cpp \
       k_induction.cpp \
       loop_utils.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -86,6 +86,7 @@ Author: Daniel Kroening, [email protected]
 #include "function.h"
 #include "havoc_loops.h"
 #include "horn_encoding.h"
+#include "insert_final_assert_false.h"
 #include "interrupt.h"
 #include "k_induction.h"
 #include "mmio.h"
@@ -257,6 +258,20 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
+    if(cmdline.isset("insert-final-assert-false"))
+    {
+      log.status() << "Inserting final assert false" << messaget::eom;
+      bool fail = insert_final_assert_false(
+        goto_model,
+        cmdline.get_value("insert-final-assert-false"),
+        ui_message_handler);
+      if(fail)
+      {
+        return CPROVER_EXIT_INTERNAL_ERROR;
+      }
+      // otherwise, fall-through to write new binary
+    }
+
     if(cmdline.isset("show-value-sets"))
     {
       do_indirect_call_and_rtti_removal();
@@ -1648,6 +1663,7 @@ void goto_instrument_parse_optionst::help()
     " --undefined-function-is-assume-false\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "                              convert each call to an undefined function to assume(false)\n"
+    HELP_INSERT_FINAL_ASSERT_FALSE
     HELP_REPLACE_FUNCTION_BODY
     HELP_ANSI_C_LANGUAGE
     "\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "aggressive_slicer.h"
 #include "generate_function_bodies.h"
+#include "insert_final_assert_false.h"
 
 #include "count_eloc.h"
 
@@ -59,6 +60,7 @@ Author: Daniel Kroening, [email protected]
   "(max-var):(max-po-trans):(ignore-arrays)" \
   "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)(reachable-call-graph)" \
+  OPT_INSERT_FINAL_ASSERT_FALSE \
   OPT_SHOW_CLASS_HIERARCHY \
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(nondet-volatile)(isr):" \

src/goto-instrument/insert_final_assert_false.cpp

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Insert assert(false) at end of entry function
+
+Author: Nathan Chong, Kareem Khazem
+
+\*******************************************************************/
+
+/// \file
+/// Insert final assert false into a function
+
+#include "insert_final_assert_false.h"
+
+#include <goto-programs/goto_model.h>
+#include <util/irep.h>
+
+#include <iterator>
+#include <list>
+
+insert_final_assert_falset::insert_final_assert_falset(
+  message_handlert &_message_handler)
+  : log(_message_handler)
+{
+}
+
+bool insert_final_assert_falset::
+operator()(goto_modelt &goto_model, const std::string &function_to_instrument)
+{
+  const irep_idt entry(function_to_instrument);
+  auto it = goto_model.goto_functions.function_map.find(entry);
+  if(it == goto_model.goto_functions.function_map.end())
+  {
+    log.error() << "insert-final-assert-false: could not find function "
+                << "'" << function_to_instrument << "'" << messaget::eom;
+    return true;
+  }
+  goto_programt &entry_function = (it->second).body;
+  goto_programt::instructionst &instructions = entry_function.instructions;
+  auto instr_it = instructions.end();
+  auto last_instruction = std::prev(instr_it);
+  DATA_INVARIANT(
+    last_instruction->is_end_function(),
+    "last instruction in function should be END_FUNCTION");
+  source_locationt assert_location = last_instruction->source_location;
+  assert_location.set_property_class(ID_assertion);
+  assert_location.set_comment("insert-final-assert-false (should fail) ");
+  goto_programt::instructiont false_assert =
+    goto_programt::make_assertion(false_exprt(), assert_location);
+  entry_function.insert_before_swap(last_instruction, false_assert);
+  return false;
+}
+
+bool insert_final_assert_false(
+  goto_modelt &goto_model,
+  const std::string &function_to_instrument,
+  message_handlert &message_handler)
+{
+  insert_final_assert_falset ifaf(message_handler);
+  return ifaf(goto_model, function_to_instrument);
+}

src/goto-instrument/insert_final_assert_false.h

@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+Module: Insert assert(false) at end of entry function
+
+Author: Nathan Chong, Kareem Khazem
+
+\*******************************************************************/
+
+/// \file
+/// Insert final assert false into a function
+
+/// This transform can be used to check for some cases of vacuous proofs
+/// Usually the given function is the test harness / entry point
+/// The instrumented assert is expected to fail
+/// If it does not then this may indicate inconsistent assumptions
+
+#ifndef CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
+#define CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H
+
+#include <string>
+
+#include <util/message.h>
+
+class goto_modelt;
+
+class insert_final_assert_falset
+{
+public:
+  explicit insert_final_assert_falset(message_handlert &_message_handler);
+  bool operator()(goto_modelt &, const std::string &);
+
+private:
+  messaget log;
+};
+
+/// Transform a goto program by inserting assert(false) at the end of a given
+/// function \p function_to_instrument. The instrumented assert is expected
+/// to fail. If it does not then this may indicate inconsistent assumptions.
+///
+/// \param goto_model: The goto program to modify.
+/// \param function_to_instrument: Name of the function to instrument.
+/// \param message_handler: Handles logging.
+/// \returns false on success
+bool insert_final_assert_false(
+  goto_modelt &goto_model,
+  const std::string &function_to_instrument,
+  message_handlert &message_handler);
+
+// clang-format off
+#define OPT_INSERT_FINAL_ASSERT_FALSE \
+  "(insert-final-assert-false):"
+
+#define HELP_INSERT_FINAL_ASSERT_FALSE \
+  " --insert-final-assert-false <function>\n" \
+  /* NOLINTNEXTLINE(whitespace/line_length) */ \
+  "                              generate assert(false) at end of function\n"
+// clang-format on
+
+#endif // CPROVER_GOTO_INSTRUMENT_INSERT_FINAL_ASSERT_FALSE_H