Translation of array_of_exprt to SMT 2 backend #7079

esteffin · 2022-08-18T17:52:04Z

Translation of array_of_exprt to SMT 2 backend

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2022-08-20T01:32:12Z

Codecov Report

Merging #7079 (8858379) into develop (12fae74) will increase coverage by 0.00%.
The diff coverage is 100.00%.

❗ Current head 8858379 differs from pull request most recent head 4f070cd. Consider uploading reports for the commit 4f070cd to get more accurate results

@@           Coverage Diff            @@
##           develop    #7079   +/-   ##
========================================
  Coverage    77.84%   77.85%           
========================================
  Files         1574     1574           
  Lines       181181   181235   +54     
========================================
+ Hits        141045   141099   +54     
  Misses       40136    40136

Impacted Files	Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	`82.35% <ø> (ø)`
..._incremental/smt2_incremental_decision_procedure.h	`75.00% <ø> (ø)`
src/ansi-c/c_typecheck_expr.cpp	`77.35% <100.00%> (+0.09%)`	⬆️
src/goto-instrument/contracts/contracts.cpp	`94.31% <100.00%> (+<0.01%)`	⬆️
...ncremental/smt2_incremental_decision_procedure.cpp	`95.98% <100.00%> (+0.29%)`	⬆️
...ncremental/smt2_incremental_decision_procedure.cpp	`98.00% <100.00%> (+0.16%)`	⬆️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

thomasspriggs · 2022-08-22T10:16:36Z

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -906,6 +906,9 @@ static smt_termt convert_expr_to_smt(
  const array_of_exprt &array_of,
  const sub_expression_mapt &converted)
 {
+  // This function is left unimplemented as the `array_of_exprt` nodes are fully


unimplemented is the wrong description of this IMO. This is because it implies an intention to implement it at some point in the future. The expectation should really be that this is UNREACHABLE due to already having been converted separately in the decision procedure.

or possibly "UNEXPECTEDCASE"

Changed the comment accordingly This function is unreachable as the array_of_exprt nodes are already.

Changed the UNIMPLEMENTED_FEATURE to UNHANDLED_CASE.

thomasspriggs · 2022-08-22T10:25:03Z

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

-  void define_array_function(const array_exprt &array);
+  /// \note Statically fails if the template type is not a `array_exprt` or
+  /// `array_of_exprt`.
+  template <typename EXPRT>


Can you not make the template type all caps? All caps is usually reserved for the names of macros. I'd also prefer to use something other than capitalisation to distinguish this template parameter from the exprt class. Maybe something like array_typed_exprt? Please have a quick re-read of the "Naming" section of CODING_STANDARD.md, as I usually apply the same naming rules to template parameters as any other (non-macro) identifier in cbmc.

Changed to t_exprt

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

thomasspriggs · 2022-08-22T10:41:42Z

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

-        smt_set_logic_commandt{
-          // NOLINTNEXTLINE(whitespace/line_length)
-          smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}},
+        smt_set_logic_commandt{// NOLINTNEXTLINE(whitespace/line_length)


The // NOLINTNEXTLINE(whitespace/line_length) comment should be removed as the updated code should now fit on one line.

I missed it.
Changed

⛏️ Looks like the fix was squashed into the wrong commit.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

thomasspriggs · 2022-08-23T12:21:55Z

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

          # remove libgcc-s1, which isn't normally available in Ubuntu 18.04
          target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
          # libgcc1 uses an epoch, thus the extra 1:
          sudo apt-get install -y --allow-downgrades --reinstall gcc g++ libgcc-s1- libstdc++6=$target liblsan0=$target libtsan0=$target libcc1-0=$target libgcc1=1:$target gdb=8.1.1-0ubuntu1
-      - name: Confirm z3 solver is available and log the version installed


⛏️ I'd prefer to leave this as a separate step, as it makes it easier to find the version number and keeps this job consistent with the others.

thomasspriggs · 2022-08-23T12:23:58Z

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

+          # download the z3 python wheel package
+          wget -O z3.4.11.0.whl https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3_solver-4.11.0.0-py2.py3-none-manylinux1_x86_64.whl
+          # unpack the bundle using python
+          python -m zipfile -e z3.4.11.0.whl z3-4.11.0-content


Why use python rather than unzip?

esteffin force-pushed the esteffin/array-of-exprt branch 3 times, most recently from 719a88e to f040f77 Compare August 19, 2022 23:19

esteffin marked this pull request as ready for review August 19, 2022 23:19

esteffin requested review from peterschrammel, thomasspriggs, NlightNFotis, TGWDB and chris-ryder as code owners August 19, 2022 23:20

esteffin requested a review from a team August 19, 2022 23:20

esteffin force-pushed the esteffin/array-of-exprt branch from f040f77 to 00a791b Compare August 20, 2022 00:06

thomasspriggs reviewed Aug 22, 2022

View reviewed changes

Add missing REQUIRE statement to array_exprt test

07e4b6e

esteffin force-pushed the esteffin/array-of-exprt branch from 00a791b to 3502fc1 Compare August 22, 2022 16:51

thomasspriggs approved these changes Aug 23, 2022

View reviewed changes

esteffin force-pushed the esteffin/array-of-exprt branch from 51abfa8 to 9bbce17 Compare August 23, 2022 12:48

Add translation of array_of_exprt to SMT2

fbb0094

esteffin force-pushed the esteffin/array-of-exprt branch from 9bbce17 to 8858379 Compare August 23, 2022 13:41

Enrico Steffinlongo added 2 commits August 23, 2022 15:02

Add array_of_exprt unit and regression tests

9391c7a

Add newer z3 version on ubuntu 18.04 github action

4f070cd

esteffin force-pushed the esteffin/array-of-exprt branch from 8858379 to 4f070cd Compare August 23, 2022 14:02

TGWDB approved these changes Aug 23, 2022

View reviewed changes

esteffin merged commit 585039a into diffblue:develop Aug 23, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Translation of array_of_exprt to SMT 2 backend #7079

Translation of array_of_exprt to SMT 2 backend #7079

Uh oh!

esteffin commented Aug 18, 2022 •

edited

Loading

Uh oh!

codecov bot commented Aug 20, 2022 •

edited

Loading

Uh oh!

thomasspriggs Aug 22, 2022

Uh oh!

thomasspriggs Aug 22, 2022

Uh oh!

esteffin Aug 22, 2022

Uh oh!

thomasspriggs Aug 22, 2022

Uh oh!

esteffin Aug 22, 2022

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Aug 22, 2022

Uh oh!

esteffin Aug 22, 2022

Uh oh!

thomasspriggs Aug 23, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thomasspriggs Aug 23, 2022

Uh oh!

thomasspriggs Aug 23, 2022

Uh oh!

Uh oh!

Translation of array_of_exprt to SMT 2 backend #7079

Translation of array_of_exprt to SMT 2 backend #7079

Uh oh!

Conversation

esteffin commented Aug 18, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Aug 20, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

esteffin commented Aug 18, 2022 •

edited

Loading

codecov bot commented Aug 20, 2022 •

edited

Loading