Merge branch 'develop' into doc_8428

CHANGELOG

@@ -1,3 +1,28 @@
+# CBMC 6.2.0
+
+## What's Changed
+* Dynamic frames: do not add trivial properties by @tautschnig in https://github.com/diffblue/cbmc/pull/8413
+
+## Bug Fixes
+* Contracts/dynamic frames: do not attempt to instrument typedefs by @tautschnig in https://github.com/diffblue/cbmc/pull/8403
+* Remove dynamic_cast from bv_dimacst by @tautschnig in https://github.com/diffblue/cbmc/pull/8406
+* Remove uses of `dynamic_cast` from qualifierst hierarchy by @tautschnig in https://github.com/diffblue/cbmc/pull/8405
+* Remove Java's unnecessary languaget::parse peculiarity by @tautschnig in https://github.com/diffblue/cbmc/pull/8407
+* Solver factory: set_decision_procedure_time_limit does not require dynamic_cast by @tautschnig in https://github.com/diffblue/cbmc/pull/8409
+* Solver factory: make_satcheck_prop does not require dynamic_cast by @tautschnig in https://github.com/diffblue/cbmc/pull/8410
+* Solver factory: all solvers are stack_decision_proceduret by @tautschnig in https://github.com/diffblue/cbmc/pull/8408
+* Remove qualifierst by @tautschnig in https://github.com/diffblue/cbmc/pull/8419
+* Contracts (DFCC) regression tests: use CaDiCaL by @tautschnig in https://github.com/diffblue/cbmc/pull/8414
+* Library functions: mark them as compiled by @tautschnig in https://github.com/diffblue/cbmc/pull/8412
+* Maintain loop invariant annotation when converting do .. while by @tautschnig in https://github.com/diffblue/cbmc/pull/8417
+* CONTRACTS: redirect checks to outer write set for loops that get skipped by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8416
+* CONTRACTS: fix do while latch by @remi-delmas-3000 in https://github.com/diffblue/cbmc/pull/8420
+* Remove dynamic_cast from counterexample beautification code path by @tautschnig in https://github.com/diffblue/cbmc/pull/8421
+* Include <cstdint> for int64_t by @ismaell in https://github.com/diffblue/cbmc/pull/8426
+* SMT2 back-end: fix inconsistent array flattening by @tautschnig in https://github.com/diffblue/cbmc/pull/8400
+
+**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.1.1...cbmc-6.2.0
+
 # CBMC 6.1.1
 
 ## What's Changed

doc/doxygen-root/doxygen-markdown/doxygen-markdown-preprocessor.py

@@ -53,15 +53,15 @@ def parse_arguments():
 
 
 def pandoc(path, pandoc_write, pandoc_wrap, pandoc_filter=None):
-    args = {
-        '--write': pandoc_write,
-        '--wrap': pandoc_wrap
-    }
+    args = [
+        '--write', pandoc_write,
+        '--wrap', pandoc_wrap
+        ]
     if pandoc_filter:
-        args['--filter'] = Path(pandoc_filter).resolve()
+        args.extend(['--filter', Path(pandoc_filter).resolve()])
 
 
-    lines = subprocess.run(['pandoc', **args, path],
+    lines = subprocess.run(['pandoc', *args, path],
                            check=True,
                            text=True,
                            capture_output=True).stdout.splitlines()

jbmc/regression/CMakeLists.txt

@@ -1,4 +1,4 @@
-set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl")
 
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are

jbmc/src/CMakeLists.txt

@@ -7,7 +7,7 @@ macro(generic_includes name)
         ${JBMC_BINARY_DIR}
         ${JBMC_SOURCE_DIR}
         ${CBMC_BINARY_DIR}
-        ${CBMC_SOURCE_DIR}
+        ${CBMC_SOURCE_DIR}/src
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
         ${CUDD_INCLUDE}

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -401,13 +401,13 @@ int janalyzer_parse_optionst::doit()
   log.status() << "Generating GOTO Program" << messaget::eom;
   lazy_goto_model.load_all_functions();
 
-  std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
+  std::unique_ptr<goto_modelt> goto_model_ptr =
     lazy_goto_modelt::process_whole_model_and_freeze(
       std::move(lazy_goto_model));
   if(goto_model_ptr == nullptr)
     return CPROVER_EXIT_INTERNAL_ERROR;
 
-  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
+  goto_modelt &goto_model = *goto_model_ptr;
 
   // show it?
   if(cmdline.isset("show-symbol-table"))

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -628,12 +628,16 @@ int jbmc_parse_optionst::get_goto_program(
 
     // Move the model out of the local lazy_goto_model
     // and into the caller's goto_model
-    goto_model_ptr = lazy_goto_modelt::process_whole_model_and_freeze(
-      std::move(lazy_goto_model));
-    if(goto_model_ptr == nullptr)
+    auto final_goto_model_ptr =
+      lazy_goto_modelt::process_whole_model_and_freeze(
+        std::move(lazy_goto_model));
+    if(final_goto_model_ptr == nullptr)
       return CPROVER_EXIT_INTERNAL_ERROR;
 
-    goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
+    goto_modelt &goto_model = *final_goto_model_ptr;
+    goto_model_ptr =
+      std::unique_ptr<abstract_goto_modelt>(final_goto_model_ptr.get());
+    final_goto_model_ptr.release();
 
     if(cmdline.isset("validate-goto-model"))
     {

jbmc/unit/CMakeLists.txt

@@ -1,5 +1,5 @@
 file(GLOB_RECURSE sources "*.cpp" "*.h")
-list(APPEND sources  ${CBMC_SOURCE_DIR}/../unit/unit_tests.cpp)
+list(APPEND sources  ${CBMC_SOURCE_DIR}/unit/unit_tests.cpp)
 
 file(GLOB_RECURSE java-testing_utils "java-testing-utils/*.cpp" "java-testing-utils/*.h")
 
@@ -14,8 +14,8 @@ add_executable(java-unit ${sources})
 target_include_directories(java-unit
     PUBLIC
     ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
-    ${CBMC_SOURCE_DIR}/../unit
+    ${CBMC_SOURCE_DIR}/src
+    ${CBMC_SOURCE_DIR}/unit
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
 target_link_libraries(java-unit

jbmc/unit/java-testing-utils/CMakeLists.txt

@@ -7,5 +7,5 @@ target_link_libraries(java-testing-utils
 target_include_directories(java-testing-utils
     PUBLIC
     ${CMAKE_CURRENT_SOURCE_DIR}/..
-    ${CBMC_SOURCE_DIR}/../unit
+    ${CBMC_SOURCE_DIR}/unit
 )

regression/ansi-c/goto_convert_assert/main.c

@@ -0,0 +1,22 @@
+void __assert_fail(char *, char *, unsigned, char *);
+
+int main()
+{
+  (void)((1 < 2) || (__CPROVER_assert(0, ""), 0));
+
+  int jumpguard;
+  jumpguard = (jumpguard | 1);
+label_1:;
+  {
+    while(1)
+    {
+      if(jumpguard == 0)
+      {
+        __assert_fail("0", "lc2.c", 8U, "func");
+        goto label_1;
+      }
+      goto label_2;
+    }
+  label_2:;
+  }
+}

regression/ansi-c/goto_convert_assert/test.desc

@@ -0,0 +1,7 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/libcprover-cpp/CMakeLists.txt

@@ -4,13 +4,13 @@ cprover_default_properties(api-binary-driver)
 target_include_directories(api-binary-driver
     PUBLIC
     ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
+    ${CBMC_SOURCE_DIR}/src
     # TODO: Should be fixed for the proper include form.
     ${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)
 target_link_libraries(api-binary-driver goto-programs util langapi ansi-c cprover-api-cpp)
 
 # Enable test running
-set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+set(test_pl_path "${CBMC_SOURCE_DIR}/regression/test.pl")
 
 macro(add_test_pl_profile name cmdline flag profile)
     add_test(

src/CMakeLists.txt

@@ -1,5 +1,3 @@
-project(CBMC VERSION ${CBMC_VERSION})
-
 find_package(BISON REQUIRED)
 find_package(FLEX REQUIRED)
 
@@ -66,8 +64,8 @@ endmacro(generic_flex)
 macro(generic_includes name)
     target_include_directories(${name}
         PUBLIC
-        ${CBMC_BINARY_DIR}
-        ${CBMC_SOURCE_DIR}
+        ${CBMC_BINARY_DIR}/src
+        ${CBMC_SOURCE_DIR}/src
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
     )

src/ansi-c/goto-conversion/goto_clean_expr.cpp

@@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     "' must be Boolean, but got ",
     irep_pretty_diagnosticst{expr});
 
+  const source_locationt source_location = expr.find_source_location();
+
   // re-write "a ==> b" into a?b:1
   if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
   {
     expr = if_exprt{
       std::move(implies->lhs()),
       std::move(implies->rhs()),
-      true_exprt{},
+      true_exprt{}.with_source_location(source_location),
       bool_typet{}};
     return;
   }
@@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
   else // ID_or
     tmp = false_exprt();
 
+  tmp.add_source_location() = source_location;
+
   exprt::operandst &ops = expr.operands();
 
   // start with last one
@@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     DATA_INVARIANT_WITH_DIAGNOSTICS(
       op.is_boolean(),
       "boolean operators must have only boolean operands",
-      expr.find_source_location());
+      source_location);
 
     if(expr.id() == ID_and)
     {
-      if_exprt if_e(op, tmp, false_exprt());
+      exprt if_e =
+        if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
+          .with_source_location(source_location);
       tmp.swap(if_e);
       continue;
     }
     if(expr.id() == ID_or)
     {
-      if_exprt if_e(op, true_exprt(), tmp);
+      exprt if_e =
+        if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
+          .with_source_location(source_location);
       tmp.swap(if_e);
       continue;
     }

src/ansi-c/goto-conversion/goto_convert.cpp

@@ -1812,8 +1812,11 @@ void goto_convertt::generate_ifthenelse(
   if(
     is_empty(false_case) && true_case.instructions.size() == 2 &&
     true_case.instructions.front().is_assert() &&
-    true_case.instructions.front().condition().is_false() &&
+    simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
     true_case.instructions.front().labels.empty() &&
+    true_case.instructions.back().is_other() &&
+    true_case.instructions.back().get_other().get_statement() ==
+      ID_expression &&
     true_case.instructions.back().labels.empty())
   {
     true_case.instructions.front().condition_nonconst() = boolean_negate(guard);

src/config.inc

@@ -79,7 +79,7 @@ endif
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
 
 # Detailed version information
-CBMC_VERSION = 6.1.1
+CBMC_VERSION = 6.2.0
 
 # Use the CUDD library for BDDs, can be installed using `make -C src cudd-download`
 # CUDD = ../../cudd-3.0.0

src/goto-instrument/contracts/contracts.cpp

@@ -68,10 +68,6 @@ void code_contractst::check_apply_loop_contracts(
   // at the start of and end of a loop body
   std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
 
-  // replace bound variables by fresh instances
-  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-    add_quantified_variable(symbol_table, invariant, mode);
-
   // instrument
   //
   //   ... preamble ...
@@ -571,13 +567,6 @@ static void generate_contract_constraints(
   goto_programt &program,
   const source_locationt &location)
 {
-  if(
-    has_subexpr(instantiated_clause, ID_exists) ||
-    has_subexpr(instantiated_clause, ID_forall))
-  {
-    add_quantified_variable(symbol_table, instantiated_clause, mode);
-  }
-
   goto_programt constraint;
   if(location.get_property_class() == ID_assume)
   {

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -235,9 +235,6 @@ dfcc_instrument_loopt::add_prehead_instructions(
   //   GOTO HEAD;
   // ```
 
-  // Replace bound variables by fresh instances in quantified formulas.
-  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-    add_quantified_variable(symbol_table, invariant, language_mode);
   // initialize loop_entry history vars;
   auto replace_history_result = replace_history_loop_entry(
     symbol_table, invariant, loop_head_location, language_mode);
@@ -429,9 +426,6 @@ dfcc_instrument_loopt::add_step_instructions(
     dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
   {
     // Assume the loop invariant after havocing the state.
-    // Replace bound variables by fresh instances in quantified formulas.
-    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assumet assumption{invariant};
     assumption.add_source_location() = loop_head_location;
     converter.goto_convert(assumption, step_instrs, language_mode);
@@ -513,9 +507,6 @@ void dfcc_instrument_loopt::add_body_instructions(
       id2string(check_location.get_function()) + "." +
       std::to_string(cbmc_loop_id));
     // Assume the loop invariant after havocing the state.
-    // Replace bound variables by fresh instances in quantified formulas.
-    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assertt assertion{invariant};
     assertion.add_source_location() = check_location;
     converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -555,13 +555,6 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   {
     exprt requires_lmbd =
       to_lambda_expr(r).application(contract_lambda_parameters);
-    requires_lmbd.add_source_location() = r.source_location();
-    if(
-      has_subexpr(requires_lmbd, ID_exists) ||
-      has_subexpr(requires_lmbd, ID_forall))
-      add_quantified_variable(
-        goto_model.symbol_table, requires_lmbd, language_mode);
-
     source_locationt sl(r.source_location());
     if(statement_type == ID_assert)
     {
@@ -609,9 +602,6 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
                       .application(contract_lambda_parameters)
                       .with_source_location(e);
 
-    if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
-      add_quantified_variable(goto_model.symbol_table, ensures, language_mode);
-
     // this also rewrites ID_old expressions to fresh variables
     generate_history_variables_initialization(
       goto_model.symbol_table, ensures, language_mode, history);

src/goto-instrument/contracts/utils.cpp

@@ -381,48 +381,6 @@ void widen_assigns(assignst &assigns, const namespacet &ns)
   assigns = result;
 }
 
-void add_quantified_variable(
-  symbol_table_baset &symbol_table,
-  exprt &expression,
-  const irep_idt &mode)
-{
-  auto visitor = [&symbol_table, &mode](exprt &expr) {
-    if(expr.id() != ID_exists && expr.id() != ID_forall)
-      return;
-    // When a quantifier expression is found, create a fresh symbol for each
-    // quantified variable and rewrite the expression to use those fresh
-    // symbols.
-    auto &quantifier_expression = to_quantifier_expr(expr);
-    std::vector<symbol_exprt> fresh_variables;
-    fresh_variables.reserve(quantifier_expression.variables().size());
-    for(const auto &quantified_variable : quantifier_expression.variables())
-    {
-      // 1. create fresh symbol
-      symbolt new_symbol = get_fresh_aux_symbol(
-        quantified_variable.type(),
-        id2string(quantified_variable.source_location().get_function()),
-        "tmp_cc",
-        quantified_variable.source_location(),
-        mode,
-        symbol_table);
-
-      // 2. add created fresh symbol to expression map
-      fresh_variables.push_back(new_symbol.symbol_expr());
-    }
-
-    // use fresh symbols
-    exprt where = quantifier_expression.instantiate(fresh_variables);
-
-    // recursively check for nested quantified formulae
-    add_quantified_variable(symbol_table, where, mode);
-
-    // replace previous variables and body
-    quantifier_expression.variables() = fresh_variables;
-    quantifier_expression.where() = std::move(where);
-  };
-  expression.visit_pre(visitor);
-}
-
 static void replace_history_parameter_rec(
   symbol_table_baset &symbol_table,
   exprt &expr,