[WISL] bi-abduction + compiler fixes

[ggwg]

In this PR

Add invalid pointer check on property lookup for WISL compiler. (As discussed in meeting with Sacha on Feb 6)

Explanation / Evaluation

Google Doc

How to generate specs:

2 test cases are located under wisl/examples/biabduction/

esy x wisl act wisl/examples/biabduction/read.wisl -o act.gil --specs-to-stdout

esy x wisl act wisl/examples/biabduction/write.wisl -o act.gil --specs-to-stdout

Code	Terminal Output

Compiler Change Example

Program Under Test

 function llen(x) {
    if (x = null) {
        n := 0
    } else {
        t := [x+1];
        n := llen(t);
        n := n + 1
    };
    return n
}

Before	New Change
``` proc llen(x) { goto [(x = null)] then0 else0; then0: n := 0i; goto endif0; else0: gvar0 := "i__add"(x, 1i); gvar1 := [getcell](l-nth(gvar0, 0i), l-nth(gvar0, 1i)); t := l-nth(gvar1, 2i); n := "llen"(t); gvar2 := "i__add"(n, 1i); n := gvar2; endif0: skip; ret := n; return }; ```	``` proc llen(x) { goto [(x = null)] then0 else0; then0: n := 0i; goto endif0; else0: gvar0 := "i__add"(x, 1i); goto [((typeOf gvar0) = List)] fail0 continue0; fail0: fail [InvalidPointer](); continue0: gvar1 := [getcell](l-nth(gvar0, 0i), l-nth(gvar0, 1i)); t := l-nth(gvar1, 2i); n := "llen"(t); gvar2 := "i__add"(n, 1i); n := gvar2; endif0: skip; ret := n; return }; ```

The new llen procedure should check the type of the input argument and fail with an InvalidPointer error if it is not a list. This is done by adding a type check to the beginning of the procedure. If the type check passes, then the procedure can proceed as normal.

[ggwg]

Q: Whats the standard procedure to test that this compiler change doesn't break anything?

[NatKarmios]

Q: Whats the standard procedure to test that this compiler change doesn't break anything?

Obviously it should compile (esy), and then esy test will run a wisl verification (as well as tests for other languages, you don't need to worry about them) to check it all works out. This provides a reasonable degree of confidence, though it'd also be a good idea for you to verify a program that uses whatever compilation has been altered (we can talk about this tomorrow).

esy test is run automatically by the build job, and I see that it's passing here.

[giltho]

Just realised @NatKarmios, how is this change going to affect the debugger?

[NatKarmios]

As long as the annots are correct, it should all work fine. I'll happily test it once this is ready for review.

[giltho]

We're ready to merge that aren't we?

[ggwg]

Ready for review. Changes since last version:

• Merge with master
• Update PR description, include Google document
• Clean code by removing all unnecessary comments