Merge pull request #15705 from ethereum/smt-fix-translation

SMTChecker: Fix parsing of array select and store expressions

Author: blishko

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
 Bugfixes:
  * General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
  * SMTChecker: Fix SMT logic error when initializing a fixed-sized-bytes array using string literals.
+ * SMTChecker: Fix SMT logic error when translating invariants involving array store and select operations.
  * Standard JSON Interface: Fix ``generatedSources`` and ``sourceMap`` being generated internally even when not requested.
  * Yul: Fix internal compiler error when a code generation error should be reported instead.
 

libsmtutil/CHCSmtLib2Interface.cpp

@@ -355,6 +355,16 @@ smtutil::Expression CHCSmtLib2Interface::ScopedParser::toSMTUtilExpression(SMTLi
 						auto accessor = maybeTupleAccessor.value();
 						return smtutil::Expression("dt_accessor_" + accessor.first, std::move(arguments), accessor.second);
 					}
+					if (op == "select")
+					{
+						smtSolverInteractionRequire(arguments.size() == 2, "Select has two arguments: array and index");
+						return smtutil::Expression::select(arguments[0], arguments[1]);
+					}
+					if (op == "store")
+					{
+						smtSolverInteractionRequire(arguments.size() == 3, "Store has three arguments: array, index and element");
+						return smtutil::Expression::store(arguments[0], arguments[1], arguments[2]);
+					}
 					else
 					{
 						std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"};

test/libsolidity/smtCheckerTests/invariants/array_access_2.sol

@@ -0,0 +1,22 @@
+contract C {
+  constructor() {
+    int8 v;
+    (v *= v);
+  }
+}
+
+contract D {
+  bool[2] internal a;
+
+  function f() internal view {
+    do {} while(!(a[1]));
+  }
+}
+// ====
+// SMTEngine: chc
+// SMTIgnoreInv: no
+// SMTSolvers: z3
+// SMTTargets: overflow
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1180: Contract invariant(s) for :D:\n(true || true)\nReentrancy property(ies) for :C:\n((<errorCode> = 0) && (x!5 = x!4))\nReentrancy property(ies) for :D:\n((<errorCode> = 0) && (x!6 = x!4) && (a' = a))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Overflow at v *= v\n