Allow writing function contracts in webassembly code

[Laplace-Demon]

No description provided.

[Laplace-Demon]

(module
    (@contract $plus_three
        (ensures (= result (+ (param 0) 3)))
    )
    (func $plus_three
        (param $x i32) (result i32)
        (i32.add (i32.const 3) (local.get $x)))
    (func $f1)
    (func $f2)
    (func $start
        (call $plus_three (i32.const 42))
        drop)
    (start $start)
)

https://github.com/OCamlPro/owi/pull/407/files#diff-7c2dae9082c169cc2debcfa373c659698275723c46bacea33467d954f5dcf87cR506

I'm expecting get _ modul.func (Text "plus_three") or get _ modul.func (Raw 0) to return the function $plus_three. But now it returns the function $start.

Upd: I mistook the use of get. It returns the i-th object of the indexed list, while we should use Indexed.get_at here.

[zapashcanon]

Thanks! I think you can add something in CHANGES.md. Also, could you add an example as you did for E-ACSL?

[zapashcanon]

Perfect! Could you add a small test with a .wat file containing an assert and call it with owi run --rac to simply check that it works correctly ? (Or it can simply contains some code with Weasel specifications, which should generate the assert)

[zapashcanon]

One more thing I am thinking of, instead of requiring an assert function from the host in the concrete case, we could simply compile the code to if (!cond) then unreachable, right?

[Laplace-Demon]

One more thing I am thinking of, instead of requiring an assert function from the host in the concrete case, we could simply compile the code to if (!cond) then unreachable, right?

Yes, but that depends on how we want our assert? Passing some meta-information of assertion (such as to which clause and contract it corresponds) may be useful, in E-ACSL they register 1. whether a failure of this assertion block the execution 2. the specification clause 3. the file name 4. the line number. For me I think showing the failing specification may be of help

[zapashcanon]

@Laplace-Demon, I wanted to merge this but it seems there's an issue with some tests from the custom-annotation proposal (see the logs in the CI). Do you want to have a look before I merge or do you prefer to fix it later?

[Laplace-Demon]

@Laplace-Demon, I wanted to merge this but it seems there's an issue with some tests from the custom-annotation proposal (see the logs in the CI). Do you want to have a look before I merge or do you prefer to fix it later?

Yes, I think we've already discussed that during my internship and all the failed tests are due to error messages different from that of the reference interpreter.

Since there are no false positives (and false negatives), I think it's okay to merge it for now. Though a fix does not amount to simply changing our error messages, but would probably require some structural change of our parser and lexer.

[zapashcanon]

Oh, OK sorry, I forget about that. But I remember now. I'm merging, thanks! :)