Merge branch 'diffblue:develop' into develop

Author: yvizel

.github/workflows/coverage.yaml

@@ -66,7 +66,7 @@ jobs:
           echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
           cmake --build build --target coverage -- -j${{env.linux-vcpus}}
       - name: Upload coverage statistics to Codecov
-        uses: codecov/codecov-action@v4
+        uses: codecov/codecov-action@v5
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
           files: build/html/coverage.info

.github/workflows/release-packages.yaml

@@ -6,6 +6,77 @@ env:
 
 name: Upload additional release assets
 jobs:
+  ubuntu-24_04-package:
+    runs-on: ubuntu-24.04
+    env:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
+          rm cvc5-Linux-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG
+          restore-keys:
+            ${{ runner.os }}-24.04-Release-${{ github.ref }}
+            ${{ runner.os }}-24.04-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure CMake
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build using Ninja
+        run: ninja -C build -j4
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run CTest
+        run: cd build; ctest . -V -L CORE -C Release -j4
+      - name: Create packages
+        id: create_packages
+        run: |
+          cd build
+          ninja package
+          deb_package_name="$(ls *.deb)"
+          echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT
+          echo "deb_package_name=ubuntu-24.04-$deb_package_name" >> $GITHUB_OUTPUT
+      - name: Get release info
+        id: get_release_info
+        uses: bruceadams/[email protected]
+      - name: Upload binary packages
+        uses: actions/upload-release-asset@v1
+        with:
+          upload_url: ${{ steps.get_release_info.outputs.upload_url }}
+          asset_path: ${{ steps.create_packages.outputs.deb_package }}
+          asset_name: ${{ steps.create_packages.outputs.deb_package_name }}
+          asset_content_type: application/x-deb
+      - name: Slack notification of CI status
+        uses: rtCamp/action-slack-notify@v2
+        if: success() || failure()
+        env:
+          SLACK_CHANNEL: aws-cbmc
+          SLACK_COLOR: ${{ job.status }}
+          SLACK_USERNAME: Github Actions CI bot
+          SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }}
+          SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 package built and uploaded successfully' || 'Ubuntu 24.04 package build failed' }}"
+
   ubuntu-22_04-package:
     runs-on: ubuntu-22.04
     env:

CHANGELOG

@@ -1,3 +1,23 @@
+# CBMC 6.4.1
+
+This patch release addresses a hard-coding of C semantics in the back-end for pointer subtraction (via #8497).
+
+## Bug Fixes
+* fix `update_bit` lowering by @kroening in https://github.com/diffblue/cbmc/pull/8496
+* Pointer subtraction in back-end: no need for bounds checking by @tautschnig in https://github.com/diffblue/cbmc/pull/8497
+* remove duplicate SATCHECK_* defines by @kroening in https://github.com/diffblue/cbmc/pull/8501
+* simplify bitxnor by @kroening in https://github.com/diffblue/cbmc/pull/8506
+* Reword documentation of __CPROVER_{r,w,rw}_ok by @tautschnig in https://github.com/diffblue/cbmc/pull/8472
+* simplify x^0 and x^1 by @kroening in https://github.com/diffblue/cbmc/pull/8509
+* add multi-ary constructor for `mult_exprt` by @kroening in https://github.com/diffblue/cbmc/pull/8510
+* Format bit-vectors with `[` ... `]` vector notation by @kroening in https://github.com/diffblue/cbmc/pull/8514
+* add range_type to `from_integer`/`to_integer` by @kroening in https://github.com/diffblue/cbmc/pull/8520
+* Bump codecov/codecov-action from 4 to 5 by @dependabot in https://github.com/diffblue/cbmc/pull/8507
+* CONTRACTS: add doc for loop assigns inference by @qinheping in https://github.com/diffblue/cbmc/pull/8516
+* Cadical with preprocessor and local search by @kroening in https://github.com/diffblue/cbmc/pull/8502
+
+**Full Changelog**: https://github.com/diffblue/cbmc/compare/cbmc-6.4.0...cbmc-6.4.1
+
 # CBMC 6.4.0
 
 This release improves upon automated assigns-clause inference for loop invariants, which should make manually adding assigns clauses to loops less frequent.

doc/cprover-manual/memory-primitives.md

@@ -233,11 +233,11 @@ number of bytes:
 - `_Bool __CPROVER_w_ok(const void *p, size_t size)`
 
 At present, both primitives are equivalent as all memory in CBMC is considered
-both readable and writeable. If `p` is the null pointer, the primitives return
-false. If `p` is valid, the primitives return true if the memory segment
-starting at the pointer has at least the given size, and false otherwise. If `p`
-is neither null nor valid, the semantics is unspecified. It is valid to apply
-the primitive to pointers that point to within a memory object. For example:
+both readable and writeable. The primitives return true if `p` points to a live
+object and the object that `p` points into extends to at least `size` more
+bytes. Else, an assertion encompassing the primitive will be reported to fail.
+Do not use these primitives in assumptions when `p` can be not valid as such use
+can yield spurious verification results.
 
 ```C
 char *p = malloc(10);

regression/cbmc/enum_is_in_range/enum_lhs.c

@@ -0,0 +1,17 @@
+enum my_enum
+{
+  A = 1,
+  B = 2
+};
+int my_array[10];
+
+int main()
+{
+  // should fail
+  (enum my_enum)3;
+
+  // should fail
+  my_array[(enum my_enum)4] = 10;
+
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_lhs.desc

@@ -0,0 +1,8 @@
+CORE
+enum_lhs.c
+--enum-range-check
+^\[main\.enum-range-check\.2\] line 14 enum range check in \(enum my_enum\)4: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

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

@@ -157,11 +157,13 @@ class goto_check_ct
   ///   guard.
   /// \param expr: the expression to be checked
   /// \param guard: the condition for when the check should be made
-  void check_rec(const exprt &expr, const guardt &guard);
+  /// \param is_assigned: the expression is assigned to
+  void check_rec(const exprt &expr, const guardt &guard, bool is_assigned);
 
   /// Initiate the recursively analysis of \p expr with its `guard' set to TRUE.
   /// \param expr: the expression to be checked
-  void check(const exprt &expr);
+  /// \param is_assigned: the expression is assigned to
+  void check(const exprt &expr, bool is_assigned);
 
   struct conditiont
   {
@@ -183,7 +185,7 @@ class goto_check_ct
   void float_div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
-  void enum_range_check(const exprt &, const guardt &);
+  void enum_range_check(const exprt &, const guardt &, bool is_assigned);
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const binary_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
@@ -537,11 +539,17 @@ void goto_check_ct::float_div_by_zero_check(
     guard);
 }
 
-void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
+void goto_check_ct::enum_range_check(
+  const exprt &expr,
+  const guardt &guard,
+  bool is_assigned)
 {
   if(!enable_enum_range_check)
     return;
 
+  if(is_assigned)
+    return; // not in range yet
+
   // we might be looking at a lowered enum_is_in_range_exprt, skip over these
   const auto &pragmas = expr.source_location().get_pragmas();
   for(const auto &d : pragmas)
@@ -1807,13 +1815,13 @@ void goto_check_ct::check_rec_address(const exprt &expr, const guardt &guard)
 
   if(expr.id() == ID_dereference)
   {
-    check_rec(to_dereference_expr(expr).pointer(), guard);
+    check_rec(to_dereference_expr(expr).pointer(), guard, false);
   }
   else if(expr.id() == ID_index)
   {
     const index_exprt &index_expr = to_index_expr(expr);
     check_rec_address(index_expr.array(), guard);
-    check_rec(index_expr.index(), guard);
+    check_rec(index_expr.index(), guard, false);
   }
   else
   {
@@ -1843,7 +1851,7 @@ void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
       return guard(implication(conjunction(constraints), expr));
     };
 
-    check_rec(op, new_guard);
+    check_rec(op, new_guard, false);
 
     constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
   }
@@ -1855,20 +1863,20 @@ void goto_check_ct::check_rec_if(const if_exprt &if_expr, const guardt &guard)
     if_expr.cond().is_boolean(),
     "first argument of if must be boolean, but got " + if_expr.cond().pretty());
 
-  check_rec(if_expr.cond(), guard);
+  check_rec(if_expr.cond(), guard, false);
 
   {
     auto new_guard = [&guard, &if_expr](exprt expr) {
       return guard(implication(if_expr.cond(), std::move(expr)));
     };
-    check_rec(if_expr.true_case(), new_guard);
+    check_rec(if_expr.true_case(), new_guard, false);
   }
 
   {
     auto new_guard = [&guard, &if_expr](exprt expr) {
       return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
     };
-    check_rec(if_expr.false_case(), new_guard);
+    check_rec(if_expr.false_case(), new_guard, false);
   }
 }
 
@@ -1878,7 +1886,7 @@ bool goto_check_ct::check_rec_member(
 {
   const dereference_exprt &deref = to_dereference_expr(member.struct_op());
 
-  check_rec(deref.pointer(), guard);
+  check_rec(deref.pointer(), guard, false);
 
   // avoid building the following expressions when pointer_validity_check
   // would return immediately anyway
@@ -1969,7 +1977,10 @@ void goto_check_ct::check_rec_arithmetic_op(
   }
 }
 
-void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
+void goto_check_ct::check_rec(
+  const exprt &expr,
+  const guardt &guard,
+  bool is_assigned)
 {
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
@@ -1980,7 +1991,7 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
       return guard(forall_exprt(quantifier_expr.symbol(), expr));
     };
 
-    check_rec(quantifier_expr.where(), new_guard);
+    check_rec(quantifier_expr.where(), new_guard, false);
     return;
   }
   else if(expr.id() == ID_address_of)
@@ -2007,10 +2018,10 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
   }
 
   for(const auto &op : expr.operands())
-    check_rec(op, guard);
+    check_rec(op, guard, false);
 
   if(expr.type().id() == ID_c_enum_tag)
-    enum_range_check(expr, guard);
+    enum_range_check(expr, guard, is_assigned);
 
   if(expr.id() == ID_index)
   {
@@ -2059,9 +2070,9 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
   }
 }
 
-void goto_check_ct::check(const exprt &expr)
+void goto_check_ct::check(const exprt &expr, bool is_assigned)
 {
-  check_rec(expr, identity);
+  check_rec(expr, identity, is_assigned);
 }
 
 void goto_check_ct::memory_leak_check(const irep_idt &function_id)
@@ -2151,7 +2162,7 @@ void goto_check_ct::goto_check(
 
     if(i.has_condition())
     {
-      check(i.condition());
+      check(i.condition(), false);
     }
 
     // magic ERROR label?
@@ -2184,45 +2195,32 @@ void goto_check_ct::goto_check(
 
       if(statement == ID_expression)
       {
-        check(code);
+        check(code, false);
       }
       else if(statement == ID_printf)
       {
         for(const auto &op : code.operands())
-          check(op);
+          check(op, false);
       }
     }
     else if(i.is_assign())
     {
       const exprt &assign_lhs = i.assign_lhs();
       const exprt &assign_rhs = i.assign_rhs();
 
-      // Disable enum range checks for left-hand sides as their values are yet
-      // to be set (by this assignment).
-      {
-        flag_overridet resetter(i.source_location());
-        resetter.disable_flag(enable_enum_range_check, "enum_range_check");
-        check(assign_lhs);
-      }
-
-      check(assign_rhs);
+      check(assign_lhs, true);
+      check(assign_rhs, false);
 
       // the LHS might invalidate any assertion
       invalidate(assign_lhs);
     }
     else if(i.is_function_call())
     {
-      // Disable enum range checks for left-hand sides as their values are yet
-      // to be set (by this function call).
-      {
-        flag_overridet resetter(i.source_location());
-        resetter.disable_flag(enable_enum_range_check, "enum_range_check");
-        check(i.call_lhs());
-      }
-      check(i.call_function());
+      check(i.call_lhs(), true);
+      check(i.call_function(), false);
 
       for(const auto &arg : i.call_arguments())
-        check(arg);
+        check(arg, false);
 
       check_shadow_memory_api_calls(i);
 
@@ -2231,7 +2229,7 @@ void goto_check_ct::goto_check(
     }
     else if(i.is_set_return_value())
     {
-      check(i.return_value());
+      check(i.return_value(), false);
       // the return value invalidate any assertion
       invalidate(i.return_value());
     }
@@ -2342,7 +2340,7 @@ void goto_check_ct::check_shadow_memory_api_calls(
   {
     const exprt &expr = i.call_arguments()[0];
     PRECONDITION(expr.type().id() == ID_pointer);
-    check(dereference_exprt(expr));
+    check(dereference_exprt(expr), false);
   }
 }