Add --insert-final-assert-false to goto-instrument

This option takes a function name (usually the test harness entry point) and
inserts `assert(false)` at the end of the function body. This assertion is
*expected to fail*. If it passes then this may indicate that the test harness
has inconsistent assumptions. Note that there are other reasons why the assert
may pass (such as insufficient loop unwind depth). It is up to the user to
interpret the results.

Author: nchong-at-aws

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