closed #450 and #197: handling big integers and better preprocessing (#…

…452)

* closed #450 and #197: handling big integers and better preprocessing

Co-authored-by: Shon Feder <shon@informal.systems>

UNRELEASED.md

@@ -10,3 +10,10 @@
          * Another change description, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Bug fixes
+
+ * handling big integers, #450
+
+### Features
+
+ * constant simplification over strings, #197

test/tla/SafeMath.tla

@@ -0,0 +1,123 @@
+---------------------------- MODULE SafeMath -----------------------------------
+(*
+ * Test that the operations over big integers go through.
+ * This specification is expected to deadlock, without violating the invariant.
+ *
+ * Here we are testing SafeMath:
+ *
+ * https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SafeMath.sol
+ *
+ * More on the topic:
+ *
+\* https://medium.com/coinmonks/math-in-solidity-part-2-overflow-3cd7283714b4
+\* https://medium.com/@soliditydeveloper.com/solidity-design-patterns-multiply-before-dividing-407980646f7
+ *
+ * Igor Konnov, 2021
+ *)
+EXTENDS Integers
+
+\* the width of the unsigned integers, like in Solidity
+BITWIDTH == 256
+POWER == 2^BITWIDTH
+MAX_UNSIGNED == (2^BITWIDTH) - 1
+
+VARIABLE opcode, arg1, arg2, res, is_error
+
+vars == <<opcode, arg1, arg2, res, is_error>>
+
+InRange(i) ==
+    i >= 0 /\ i <= MAX_UNSIGNED
+
+TryAdd(a, b) ==
+    LET c == (a + b) % POWER IN
+    IF c < a
+    THEN <<FALSE, 0>>
+    ELSE <<TRUE, c>>
+
+TrySub(a, b) ==
+    IF b > a
+    THEN <<FALSE, 0>>
+    ELSE <<TRUE, (a - b) % POWER>>
+
+TryMul(a, b) ==
+    IF a = 0
+    THEN <<TRUE, 0>>
+    ELSE LET c == (a * b) % POWER IN
+        IF c \div a /= b
+        THEN <<FALSE, 0>>
+        ELSE <<TRUE, c>>
+
+TryDiv(a, b) ==
+    IF b = 0
+    THEN <<FALSE, 0>>
+    ELSE <<TRUE, a \div b>>
+
+TryMod(a, b) ==
+    IF b = 0
+    THEN <<FALSE, 0>>
+    ELSE <<TRUE, a % b>>
+
+TestTry(code, Op(_, _)) ==
+    \* non-deterministically pick two non-negative integers
+    \E a, b \in Int:
+        /\ InRange(a)
+        /\ InRange(b)
+        /\ LET flag_and_c == Op(a, b) IN
+            /\ opcode' = code
+            /\ arg1' = a
+            /\ arg2' = b
+            /\ is_error' = ~flag_and_c[1]
+            /\ res' = flag_and_c[2]
+
+Init ==
+    /\ opcode = "NOP"
+    /\ arg1 = 0
+    /\ arg2 = 0
+    /\ res = 0
+    /\ is_error = FALSE
+
+Next ==
+    \/ /\ opcode = "NOP"
+       /\ \/ TestTry("ADD", TryAdd)
+          \/ TestTry("SUB", TrySub)
+          \* The following operators are too hard for z3 to work out
+          \* of the box. Perhaps, we have to use bitvectors.
+          (*
+          \/ TestTry("MUL", TryMul)
+          \/ TestTry("DIV", TryDiv)
+          \/ TestTry("MOD", TryMod)
+            *)
+    \/ opcode /= "NOP" /\ UNCHANGED vars
+
+InvAdd ==
+    LET perfectInt == arg1 + arg2 IN
+    opcode = "ADD"
+        => is_error <=> (perfectInt > MAX_UNSIGNED /\ res /= perfectInt)
+
+InvSub ==
+    LET perfectInt == arg1 - arg2 IN
+    opcode = "SUB"
+        => is_error <=> (perfectInt < 0 /\ res /= perfectInt)
+
+InvMul ==
+    LET perfectInt == arg1 * arg2 IN
+    opcode = "MUL"
+        => is_error <=> (perfectInt > MAX_UNSIGNED /\ res /= perfectInt)
+
+InvDiv ==
+    LET perfectInt == arg1 \div arg2 IN
+    opcode = "DIV"
+        => is_error <=>
+            arg2 = 0 \/ (perfectInt > MAX_UNSIGNED /\ res /= perfectInt)
+
+InvMod ==
+    LET perfectInt == arg1 % arg2 IN
+    opcode = "MOD"
+        => is_error <=>
+            arg2 = 0 \/ (perfectInt > MAX_UNSIGNED /\ res /= perfectInt)
+
+
+\* check this to see an overflow
+FalseInv ==
+    arg1 + arg2 < MAX_UNSIGNED
+==============================================================================

test/tla/cli-integration-tests.md

@@ -110,6 +110,24 @@ EXITCODE: OK
 ## running the check command
 
 
+### check InvSub for SafeMath reports no error: regression for issue 450
+
+```sh
+$ apalache-mc check --length=1 --inv=InvSub SafeMath.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
+### check InvAdd for SafeMath reports no error: regression for issue 450
+
+```sh
+$ apalache-mc check --length=1 --inv=InvAdd SafeMath.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+```
+
 ### check Fix365_ExistsSubset succeeds: regression for issue 365
 
 ```sh

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala

@@ -460,7 +460,8 @@ class SymbStateRewriterImpl(private var _solverContext: SolverContext,
     * @return the snapshot
     */
   override def snapshot(): SymbStateRewriterSnapshot = {
-    new SymbStateRewriterSnapshot(typeFinder.asInstanceOf[TrivialTypeFinder].snapshot(), intValueCache.snapshot(),
+    new SymbStateRewriterSnapshot(typeFinder.asInstanceOf[TrivialTypeFinder].snapshot(),
+      intValueCache.snapshot(),
       intRangeCache.snapshot(), strValueCache.snapshot(), recordDomainCache.snapshot(), exprCache.snapshot())
   }
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala

@@ -12,9 +12,9 @@ import at.forsyte.apalache.tla.lir.{OperEx, ValEx}
   *
   * @author Igor Konnov
   */
-class IntValueCache(solverContext: SolverContext) extends AbstractCache[Arena, Int, ArenaCell] with Serializable {
+class IntValueCache(solverContext: SolverContext) extends AbstractCache[Arena, BigInt, ArenaCell] with Serializable {
 
-  def create(arena: Arena, intValue: Int): (Arena, ArenaCell) = {
+  def create(arena: Arena, intValue: BigInt): (Arena, ArenaCell) = {
     // introduce a new constant
     val newArena = arena.appendCell(IntT())
     val intCell = newArena.topCell