Merge pull request #8670 from tautschnig/convert-with

SMT2 back-end: flatten with_exprt operands

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -72,9 +72,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
       - name: Check cleanup
         run: |
@@ -153,9 +154,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}}
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
 
   # This job has been copied from the one above it, and modified to only build CBMC
@@ -339,9 +341,10 @@ jobs:
           make TAGS="[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
+          export PATH=$PATH:`pwd`/src/solvers
           make -C regression test-parallel JOBS=${{env.linux-vcpus}}
           make -C regression/cbmc test-paths-lifo
-          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C regression/cbmc test-cprover-smt2
           make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
 
   # This job takes approximately 17 to 41 minutes
@@ -689,7 +692,9 @@ jobs:
       - name: Run JBMC unit tests
         run: cd jbmc/unit; ./unit_tests
       - name: Run regression tests
-        run: make -C regression test-parallel JOBS=4
+        run: |
+          export PATH=$PATH:`pwd`/src/solvers
+          make -C regression test-parallel JOBS=4
       - name: Run JBMC regression tests
         run: make -C jbmc/regression test-parallel JOBS=4
 
@@ -855,7 +860,9 @@ jobs:
       - name: Download minisat with make
         run: make -C src minisat2-download
       - name: Build CBMC with make
-        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
+        run: |
+          make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
+          echo "$pwd\src\solvers;" >> $env:GITHUB_PATH
       - name: Build unit tests with make
         run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
       - name: Build jbmc with make

regression/contracts-dfcc/CMakeLists.txt

@@ -41,10 +41,15 @@ add_test_pl_profile(
 #)
 
 # solver appears on the PATH in Windows already
-#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-#  set_property(
-#    TEST "cbmc-cprover-smt2-CORE"
-#    PROPERTY ENVIRONMENT
-#      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
-#  )
-#endif()
+if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set_property(
+    TEST "contracts-dfcc-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+  set_property(
+    TEST "contracts-non-dfcc-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+endif()

regression/contracts-dfcc/array_struct_smt-02/main.c

@@ -0,0 +1,24 @@
+typedef struct
+{
+  int coeffs[1];
+} mld_poly;
+
+typedef struct
+{
+  mld_poly vec[1];
+} mld_polyveck;
+
+int main()
+{
+  mld_polyveck h;
+
+  // clang-format off
+  for(unsigned int i = 0; i < 1; ++i)
+    __CPROVER_loop_invariant(i <= 1)
+  {
+    h.vec[i].coeffs[0] = 1;
+  }
+  // clang-format on
+
+  return 0;
+}

regression/contracts-dfcc/array_struct_smt-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts _ --cprover-smt2
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Make sure the SMT back-end produces valid SMT2 when structs and arrays are
+nested in each other.

regression/contracts-dfcc/array_struct_smt/main.c

@@ -0,0 +1,17 @@
+typedef struct
+{
+  int coeffs[2];
+} mlk_poly;
+
+// clang-format off
+void mlk_poly_add(mlk_poly *r, const mlk_poly *b)
+  __CPROVER_ensures(r->coeffs[0] == __CPROVER_old(*r).coeffs[0] + b->coeffs[0])
+  __CPROVER_assigns(__CPROVER_object_upto(r, sizeof(mlk_poly)));
+// clang-format on
+
+int main()
+{
+  mlk_poly r[1];
+  mlk_poly b[1];
+  mlk_poly_add(&r[0], &b[0]);
+}

regression/contracts-dfcc/array_struct_smt/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --replace-call-with-contract mlk_poly_add _ --no-array-field-sensitivity --cprover-smt2
+^\[mlk_poly_add.overflow.1\] line 8 arithmetic overflow on signed \+
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Make sure the SMT back-end produces valid SMT2 when structs and arrays are
+nested in each other.

src/solvers/smt2/smt2_conv.cpp

@@ -1407,9 +1407,35 @@ void smt2_convt::convert_expr(const exprt &expr)
     out << "(ite ";
     convert_expr(if_expr.cond());
     out << " ";
-    convert_expr(if_expr.true_case());
+    if(
+      expr.type().id() == ID_array && !use_array_theory(if_expr.true_case()) &&
+      use_array_theory(if_expr.false_case()))
+    {
+      unflatten(wheret::BEGIN, expr.type());
+
+      convert_expr(if_expr.true_case());
+
+      unflatten(wheret::END, expr.type());
+    }
+    else
+    {
+      convert_expr(if_expr.true_case());
+    }
     out << " ";
-    convert_expr(if_expr.false_case());
+    if(
+      expr.type().id() == ID_array && use_array_theory(if_expr.true_case()) &&
+      !use_array_theory(if_expr.false_case()))
+    {
+      unflatten(wheret::BEGIN, expr.type());
+
+      convert_expr(if_expr.false_case());
+
+      unflatten(wheret::END, expr.type());
+    }
+    else
+    {
+      convert_expr(if_expr.false_case());
+    }
     out << ")";
   }
   else if(expr.id()==ID_and ||
@@ -4400,50 +4426,63 @@ void smt2_convt::convert_with(const with_exprt &expr)
     }
     else
     {
+      auto convert_operand = [this](const exprt &op)
+      {
+        // may need to flatten array-theory arrays in there
+        if(op.type().id() == ID_array && use_array_theory(op))
+          flatten_array(op);
+        else if(op.type().id() == ID_bool)
+          flatten2bv(op);
+        else
+          convert_expr(op);
+      };
+
       std::size_t struct_width=boolbv_width(struct_type);
 
       // figure out the offset and width of the member
       const boolbv_widtht::membert &m =
         boolbv_width.get_member(struct_type, component_name);
 
-      out << "(let ((?withop ";
-      convert_expr(expr.old());
-      out << ")) ";
-
       if(m.width==struct_width)
       {
-        // the struct is the same as the member, no concat needed,
-        // ?withop won't be used
-        convert_expr(value);
-      }
-      else if(m.offset==0)
-      {
-        // the member is at the beginning
-        out << "(concat "
-            << "((_ extract " << (struct_width-1) << " "
-                              << m.width << ") ?withop) ";
-        convert_expr(value);
-        out << ")"; // concat
-      }
-      else if(m.offset+m.width==struct_width)
-      {
-        // the member is at the end
-        out << "(concat ";
-        convert_expr(value);
-        out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
+        // the struct is the same as the member, no concat needed
+        convert_operand(value);
       }
       else
       {
-        // most general case, need two concat-s
-        out << "(concat (concat "
-            << "((_ extract " << (struct_width-1) << " "
-                              << (m.offset+m.width) << ") ?withop) ";
-        convert_expr(value);
-        out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
-        out << ")"; // concat
-      }
+        out << "(let ((?withop ";
+        convert_operand(expr.old());
+        out << ")) ";
 
-      out << ")"; // let ?withop
+        if(m.offset == 0)
+        {
+          // the member is at the beginning
+          out << "(concat "
+              << "((_ extract " << (struct_width - 1) << " " << m.width
+              << ") ?withop) ";
+          convert_operand(value);
+          out << ")"; // concat
+        }
+        else if(m.offset + m.width == struct_width)
+        {
+          // the member is at the end
+          out << "(concat ";
+          convert_operand(value);
+          out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
+        }
+        else
+        {
+          // most general case, need two concat-s
+          out << "(concat (concat "
+              << "((_ extract " << (struct_width - 1) << " "
+              << (m.offset + m.width) << ") ?withop) ";
+          convert_operand(value);
+          out << ") ((_ extract " << (m.offset - 1) << " 0) ?withop)";
+          out << ")"; // concat
+        }
+
+        out << ")"; // let ?withop
+      }
     }
   }
   else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)