[SAL-HELP] Differences between sal-bmc and sal-inf-bmc

[Bruno Dutertre]

Ambar Gadkari wrote:
> Hello,
> 
> I am trying to understand 'sal-inf-bmc' and have found some
> strange behaviour while generating counter-examples for simple safety
> properties. I am using sal version 3.0.
> An example illustrating the issues is attached herewith.
> 
> Observations:
> case 1.
> sal-bmc -it ex.sal th1 ----- Generates CE of length 2
>  sal-inf-bmc -it ex.sal th1 ----- Also generates CE of length 2
> 
> case 2.
> sal-bmc -it ex.sal th2 ----- Generates CE of length 2
>  sal-inf-bmc -it ex.sal th2 ----- However, generates CE of length 6
> 
> case 3.
>  sal-bmc -it ex.sal th3 ----- Generates CE of length 4
>  sal-inf-bmc -it ex.sal th3 ----- Does not generate CE (also tried upto
> depth 20 w/o luck!)
> 
> Any help on clarifying these differences in cases 2 and 3 would be highly
> appreciated.
> 
> Thanks and regards,
> Ambar.
> 

Ambar,

That's a tricky problem, related to type checking and arithmetic overflow
in the boolean encoding of the modules. The specifications are not type correct,
but the tools do not detect the type error. Then, because of the way arithmetic
operations are encoded, sal-inf-bmc and sal-bmc do not behave in the same way.

In module m2, you have the assignment

     o2' = o2 + 2*i2 - o1;

with the types

     o2: [0 .. 100]
     o1: [0 .. 100]
     i2: [0 .. 10]

Both sal-bmc and sal-inf-bmc assume (incorrectly in this case) that the
type constraints are satisfied and turn them into invariants. Both will
add the constraint 0 <= o2 <= 100 as a state invariant. This rules out
any transition where o2 + 2*i2 - o1 is negative. That's what's happening
with sal-inf-bmc.

The second problem is that the translation to booleans relies on the
types to determine the number of bits necessary to represent the state
variables. In this case, 7-bits are necessary for o2. The operation
o2 + 2*i2 - o1 is then encoded as an operation on 7-bit unsigned
integers. That would be safe if the type constraint "0 <= o2' <= 100" was
actually satisfied. Since it is not, there are risks of numerical
overflow/underflow. Some state transitions can happen modulo 128 that
do not happen in ordinary arithmetic. For example, the binary encoding
in sal-bmc will allow the transition

    o2 = 3
    i2 = 1
    o1 = 42

    o2' = 91 (because 91 = -37 modulo 128)

sal-inf-bmc does not allow this transition since it does arithmetic
on the integers and enforces the constraint 0 <= o2' <= 100.
That's why sal-bmc (or sal-smc) finds counterexamples that sal-inf-bmc
does not find.

You can try to put a guard in m2's transition to prevent the arithmetic
overflow, e.g.,

  [
    0 <= o2 + 2*i2 - o1 -->
        o2' = o2 + 2*i2 - o1;
        cond2' = IF (o2' > 80) THEN TRUE ELSE FALSE ENDIF;
  ]

then sal-bmc and sal-inf-bmc should agree.

Bruno