Allow writing function contracts in webassembly code

[Laplace-Demon]

[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.

[redianthus]

I don't understand your add --add-assert-to-assume option, I believe this is something that should be done at the symbolic execution implementation level directly, you should not try to emulate it in rac.

[Laplace-Demon]

I don't understand your add --add-assert-to-assume option, I believe this is something that should be done at the symbolic execution implementation level directly, you should not try to emulate it in rac.

Okay ! When I finished I got complaint that owi_assume is never used, which made me think that --add-assert-to-assume might be something to add. I'll just mark it with _owi_assume instead

[redianthus]

I don't understand your add --add-assert-to-assume option, I believe this is something that should be done at the symbolic execution implementation level directly, you should not try to emulate it in rac.

Okay ! When I finished I got complaint that owi_assume is never used, which made me think that --add-assert-to-assume might be something to add. I'll just mark it with _owi_assume instead

OK, you can also simply remove it if it is not needed for now.

[redianthus]

This needs to be rebased

[redianthus]

So I believe we should add some stuff:

• being able to generate an instrumented version that does not depend on symbolic execution (let's call it rac for runtime assertion checking);
• being able to generate an instrumented version that does depend on symbolic execution (let's call it srac) (we already have this one);
• add an option --rac to owi run that would perform the checks;
• add options --rac and --srac to owi sym and owi conc;
• add a --symbolic option (or maybe --srac to be more consistent?) to owi rac that would generate the one that depends on symbolic execution.

Moreover, what do you think about renaming owi rac into owi instrument ?

[Laplace-Demon]

Moreover, what do you think about renaming owi rac into owi instrument ?

For the name, rac is used temporarily and not the most suitable, instrument is better

[Laplace-Demon]

So I believe we should add some stuff:

* being able to generate an instrumented version that does not depend on symbolic execution (let's call it `rac` for `runtime assertion checking`);

* being able to generate an instrumented version that does depend on symbolic execution (let's call it `srac`) (we already have this one);

* add an option `--rac` to `owi run` that would perform the checks;

* add options `--rac` and `--srac` to `owi sym` and `owi conc`;

* add a `--symbolic` option (or maybe `--srac` to be more consistent?) to `owi rac` that would generate the one that depends on symbolic execution.

Moreover, what do you think about renaming owi rac into owi instrument ?

For better visibility, we will have:

• owi instrument for instrumentation
• owi instrument --symbolic for instrumentation with owi symbolic functions
• owi run --rac, owi sym --rac and owi conc --rac for instrumentation and execution
• owi sym --srac and owi conc --srac for instrumentation and symbolic execution

[redianthus]

Could you rebase so I can merge? :)

[Laplace-Demon]

Could you rebase so I can merge? :)

I'll rebase later today, to check if there are something left :)

[redianthus]

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

[redianthus]

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)

[redianthus]

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

[redianthus]

@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.

[redianthus]

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