PSL now supports sHLL

PSL 5 with sHLL support has been released! PSL is Prover’s model-checker that allows to verify designs according to safety properties and environment constraints. It natively takes HLL designs as inputs. But here is the novelty!

With this new version of PSL, it is now possible to directly load sHLL models without an external translation phase. Potential error messages are displayed with direct reference to the sHLL file. This sHLL model can be mixed with any HLL sections such as constraints, proof obligations or lemmas.

sHLL is Prover’s imperative extension over HLL. It can be used as an intermediate step when translating designs from imperative languages (such as C or Ada) but can also be used as an input language for the formalization of imperative-style specifications. sHLL simply encapsulates HLL expressions as assignments in a setting that also defines:

– a set of global variables that could be assigned at various levels.

– procedures, that may modify some global variables, and that provides a finite while loop construction.

– statements that define a call order of these procedures.

This structure is then embedded in the natural temporal loop beneath the HLL execution model.

Consider the following HLL loop, where an array state variable state is defined recursively by a global variable global:

Inputs:
int in1;
Declarations:
int^(3) state;
Definitions:
I(state[a]) := 0;
X(state[a]) := global[a];

The following sHLL model defines how global is successively modified at each step by calls to procedure1 (which iterates over the array and adds the current input value in1 to each cell of the array), and procedure2 (which multiplies the resulting cell with the value of its index):

Globals:
int^(3) global;
Procedures:
procedure1(int in1; int^(3) global) {
    int idx;
    idx:= 0;
    while (idx <= 2)[3] {
    global[idx] := global[idx] + in1;
    idx := idx + 1;
    }
}
procedure2(; int^(3) global) {
    int idx;
    idx:= 0;
    while (idx <= 2)[3] {
    global[idx] := global[idx] * idx;
    idx := idx + 1;
    }
}
Statements:
global:=state;
procedure1(in1; global);
procedure2(;global);

At every cycle, in1 is randomly assigned to an integer value; global is evaluated by first applying the expression in procedure1, then procedure2; global is eventually passed to state to store the value at the end of an HLL cycle.  

This clear separation between the pure dataflow style of HLL and the imperative style of sHLL allows to lower the distance when dealing with high-level pieces of code. For instance, when an algorithm has been specified in C, Ada, or even in a state-based specification language like B, using sHLL is a more natural candidate both for modeling this algorithm and for checking properties. You might, for example, want to check that the following property holds:

Proof Obligations:
ALL i:[0,2] (global[i] >=i);

This proof obligation is obviously false, and when loading this model files in PSL, a counterexample can be explored using the tool Why for sHLL structures:

psl -shll model.shll -hll model.hll -intSize 16 -ind -why

[depth 0]>
$0: ALL i:[0,2] (global[i] >= i) is [f]
because:
$1: global[0] >= 0 is [t]
$2*: global[1] >= 1 is [f]
$3: global[2] >= 2 is [f]

[depth 0]>
$4: global[1] is [-32767]
because:
procedure2(; global);
and:
$6*: global[1] is [-32767]

[model.shll:26][depth 0]>
$6: global[1] is [-32767]
because:
global[idx] := global[idx] * idx;
and:
$7: idx is [1]
$8*: global[idx] * idx is [-32767]

Debugging is available at the sHLL level, allowing for backward search into root causes of this falsifiable proof obligation using the identifiers at the sHLL level, and pointing to part of the code relevant for the current state of the debugger. It is hence much easier to understand what is wrong and corrections made in the source code can be directly fed to PSL for another run until the proof obligation becomes valid.

This step forward in the direction of handling imperative programs with PSL will be followed by many other steps to keep improving the debugger, and the support for error localization in Prover Studio. See our previous blog post about that here. We are eagerly waiting for your feedback to contribute to this new feature and its integration with other Prover tools.