[SMTChecker] Study large vs small blocks for CHC branches

[leonardoalt]

When encoding the program into Horn clauses, there are two options when an if is reached:

1. Large blocks:
   • Do not create new blocks for branches and rely on the SSA scheme to implicitly encode the branches.
   • Assertions create edges from function to error.
   • Advantages: much simpler to code, the generated invariants respect the control-flow.
   • The disadvantage is constraint repetition whenever there's an edge from the function. Maybe this is optimized by the solver and is ok.
2. Small blocks:
   • Create a function block f_i containing all the constraints as long as the flow is linear; a block if for the if's entry point; blocks ifTrue and ifFalse for the true and false statements; a block f_j that continues at the join point. The edges are f_i -> if, if -> ifTrue, if -> ifFalse, ifTrue -> f_j, ifFalse -> f_j. If the if has no false statement, f_i -> f_j.
   • Advantages: no constraint repetition, more precision in the encoding.
   • Disadvantages: more complicated code, and because the if's condition is asserted in the control-flow path, it is always true in the control-flow path of assertions inside branches.

[leonardoalt]

Example:

pragma solidity >=0.5.9;
pragma experimental SMTChecker;

contract Simple {
    bool a;
    bool b;

    function f() public {
        if (!a) {
            a = true;
            b = true;
        }
    }

    function g() public {
        // 1
        //if (a) assert(b);

        // 2
        //assert(a == b);

        // 3
        //assert(!a || b);
    }
}

[leonardoalt]

Large block invariants:

1. a => b
2. a <=> b
3. a => b

[leonardoalt]

Small block invariants:

1. a /\ b
2. a <=> b
3. a /\ b

Note that 1 and 3 are wrong. At the moment I think this is because the way the encoding is implemented for small blocks, where the if condition is asserted in the control-flow path.

[leonardoalt]

Large block rules for assertion 1:

constructor_Simple_33_0

(=> (and constructor_Simple_33_0 (= b_6_1 false) (= a_4_1 false))
    (interface_Simple_33_0 a_4_1 b_6_1))

(=> (interface_Simple_33_0 a_4_3 b_6_3) (function_f_22_0 a_4_3 b_6_3))

(=> (and (function_f_22_0 a_4_3 b_6_3)
         (= b_6_5 (ite expr_10_1 b_6_4 b_6_3))
         (= a_4_5 (ite expr_10_1 a_4_4 a_4_3))
         (= b_6_4 expr_17_1)
         (= expr_17_1 expr_16_0)
         (= expr_16_0 true)
         (= a_4_4 expr_13_1)
         (= expr_13_1 expr_12_0)
         (= expr_12_0 true)
         (= expr_10_1 (not expr_9_0))
         (= expr_9_0 a_4_3)
         true)
    (interface_Simple_33_0 a_4_5 b_6_5))

(=> (interface_Simple_33_0 a_4_7 b_6_7) (function_g_32_0 a_4_7 b_6_7))

(=> (and (function_g_32_0 a_4_7 b_6_7)
         (= expr_27_0 b_6_7)
         (= expr_25_0 a_4_7)
         true
         true
         expr_25_0
         (not expr_27_0))
    error_0)

(=> (and (function_g_32_0 a_4_7 b_6_7)
         (=> (and true expr_25_0) expr_27_0)
         (= expr_27_0 b_6_7)
         (= expr_25_0 a_4_7)
         true)
    (interface_Simple_33_0 a_4_7 b_6_7))

[leonardoalt]

Small block rules for assertion 1:

constructor_Simple_33_0

(=> (and constructor_Simple_33_0 (= b_6_1 false) (= a_4_1 false))
    (interface_Simple_33_0 a_4_1 b_6_1))

(=> (interface_Simple_33_0 a_4_3 b_6_3) (function_f_22_0 a_4_3 b_6_3))

(=> (and (function_f_22_0 a_4_3 b_6_3) true) (if_20_0 a_4_3 b_6_3))

(=> (and (if_20_0 a_4_3 b_6_3)
         (= expr_10_1 (not expr_9_0))
         (= expr_9_0 a_4_3)
         true
         expr_10_1)
    (if_true_19_0 a_4_3 b_6_3))

(=> (and (if_true_19_0 a_4_3 b_6_3)
         (= b_6_4 expr_17_1)
         (= expr_17_1 expr_16_0)
         (= expr_16_0 true)
         (= a_4_4 expr_13_1)
         (= expr_13_1 expr_12_0)
         (= expr_12_0 true)
         (= expr_10_1 (not expr_9_0))
         (= expr_9_0 a_4_3)
         true)
    (function_f_22_1 a_4_4 b_6_4))

(=> (and (if_20_0 a_4_3 b_6_3)
         (= expr_10_1 (not expr_9_0))
         (= expr_9_0 a_4_3)
         true
         (not expr_10_1))
    (function_f_22_1 a_4_3 b_6_3))

(=> (and (function_f_22_1 a_4_4 b_6_4) true)
    (interface_Simple_33_0 a_4_4 b_6_4))

(=> (interface_Simple_33_0 a_4_6 b_6_6) (function_g_32_0 a_4_6 b_6_6))

(=> (and (function_g_32_0 a_4_6 b_6_6) true) (if_30_0 a_4_6 b_6_6))

(=> (and (if_30_0 a_4_6 b_6_6) (= expr_25_0 a_4_6) true expr_25_0)
    (if_true_29_0 a_4_6 b_6_6))

(=> (and (if_true_29_0 a_4_6 b_6_6)
         (= expr_27_0 b_6_6)
         (= expr_25_0 a_4_6)
         true
         true
         (not expr_27_0))
    error_0)

(=> (and (if_true_29_0 a_4_6 b_6_6)
         (=> true expr_27_0)
         (= expr_27_0 b_6_6)
         (= expr_25_0 a_4_6)
         true)
    (function_g_32_1 a_4_6 b_6_6))

(=> (and (if_30_0 a_4_6 b_6_6) (= expr_25_0 a_4_6) true (not expr_25_0))
    (function_g_32_1 a_4_6 b_6_6))

(=> (and (function_g_32_1 a_4_6 b_6_6) true)
    (interface_Simple_33_0 a_4_6 b_6_6))

[leonardoalt]

The CHC code is now stable and using small blocks. This follows CFG generation and makes the model much cleaner.