Adding ACSL contracts for SBV

[GAJaloyan]

Hi everybody,

I'm working on Copilot, a Haskell EDSL that compiles runtime monitors to C. SBV is one of our C backends and really like many of its features. We have been trying to write Contracts for the generated C code that include preconditions, postconditions, and invariants. These contracts are written in the ACSL notation and are written as C comments with the following general format /@ requires ........../ /@ ensures ........... /

We also include additional comments to help improve tracibility from Haskell monitor to the C code. However, there seems that there is no easy way to write ACSL contracts for the code generated (I'm trying to put comments when a function is created, given that there is no loops in the code produced).

I forked the SBV and worked a little bit on it here : https://github.com/Copilot-Language/sbv-for-copilot and made some changes (such as compiling logical abstract operators as logical operators and not as bitwise to improve performance of the provers in frama-c, adding the possibility to pass a comment in the compileToC function, allowing to change the compiler, and removing some double includes). The backend we use is also here https://github.com/Copilot-Language/copilot-sbv/tree/acsl and it generates the contracts to pass them to the SBV, that just copies them on the right place. It compiles with ccomp, and the value analysis plugin seems to work pretty well on the code produced.

Is it planned to have the feature of generating comments implemented in SBV (so as not to use a modified fork) soon ? Is there a way do to it without changing the prototypes of the function (backward compatibility) ?

We have also some troubles with some features not implemented (shitL, shitR with variable numbers, floats and doubles, ...).

Here is an example of the code produced : there are some ACSL, but also tracability (prettyprinting what is compiled, to know exactly what this code does).

/* File: "update_state_0.c". Automatically generated by SBV. Do not edit! */

include "internal.h"

/ACSL following/ /test 001/ /ACSL to write (if (s0 /= 4) then (s0 + 1) else 0) */ /@ assigns \nothing; ensures \result == ( (queue_0[ptr_0] != 4) ? (queue_0[ptr_0] + 1) : 0); / SWord8 update_state_0(const SWord8 queue_0, const SWord32 ptr_0) { const SWord8 s0 = queue_0[0]; const SWord32 s1 = ptr_0; const SBool s3 = s0 != 4; const SWord8 s5 = s0 + 1; const SWord8 s7 = s3 ? s5 : 0;

return s7; }

[LeventErkok]

@Varmin You can add arbitrary text before the function already via cgAddDecls. Would that do the trick?

test :: IO ()
test = compileToC Nothing "tst" $ do
            cgAddDecl [ "/* hello there  */"
                      , "/* Another line */"
                      ]
            x <- cgInput "x"
            y <- cgInput "y"
            cgReturn $ (x+y::SWord8)

Let me know if this mechanism does not suffice.

Regarding shiftL/shiftR with variable second argument: There's a nice trick you can use to handle such calls, See here: https://hackage.haskell.org/package/sbv-4.4/docs/src/Data-SBV-Examples-CodeGeneration-Uninterpreted.html#shiftLeft

Regarding doubles/floats: Latest version of SBV fully supports IEEE float/double types. (SFloat/SDouble.) Use Z3 for verification tasks regarding float/doubles. C-code generation should work just fine as well. Did you try them out? Let me know if you spot any issues. I've tested them fairly well, but there's always a gotcha. If you're using float/double's in your code, I'd recommend using the SBV version directly out of github.

[GAJaloyan]

@LeventErkok : I tried some features :

ACSL at the beginning of functions : it works well, ACSL understands it. Floats/Doubles : Implemented just the division on our backend, it seems to work, I'll make more tests today and see.

Still some issues : we cannot change the compiler without changing manually the makefile : is it possible to add this edit to the master project ? https://github.com/Copilot-Language/sbv-for-copilot/commit/ef7d30ef55fc0a9b9710b04bbe86ca1fc4bcbf75

Same about https://github.com/Copilot-Language/sbv-for-copilot/commit/5884d70ee59ae9756c7d388d8e0dd33c483b057e : the logical operations are translated into bitwise. Even if the modelchecker proves that in a bitwise form, it would be great if it compiles in logical values (but it seems that frama-c value analysis plugin does not have troubles proving bitwise operations). All the more so since a proven bitwise operation on booleans implies that everything goes well in the logical form (which is not true the other way).

An other issue : when I send something like a / 3.0, it compiles into : const SFloat s20 = (3.0F == 0) ? 0 : (s18 / 3.0F); And splint is not happy : observer_meanV.c: (in function observer_meanV) observer_meanV.c:41:24: Dangerous equality comparison involving float types: 3.0F == 0.0F Two real (float, double, or long double) values are compared directly using == or != primitive. This may produce unexpected results since floating point representations are inexact. Instead, compare the difference to FLT_EPSILON or DBL_EPSILON. (Use -realcompare to inhibit warning)

Addendum : I tried the floating operations, but they work only on constants as specified in BitVectors/Model.hs (ACSL is not able to handle them anyway). Is there a way to force the compiling of the expression (meamning that it will produce a C code for it), instead of crashing in case of a non constant operation ?

[LeventErkok]

@Varmin

Choosing the C-compiler in the Makefile: Done; don't know how we didn't do that before; I think it was @leepike who told me first about that trick.

Div-by-0 on float/double: That was an oversight; as we don't actually have to protect against in that case. Division by 0 is well-defined for float/double values (0/0=NaN, x/0=Infinity etc); so that code was just spurious. I removed it; so that problem should now go away.

Regarding LOr/LAnd: We can't just add operators, as there are implications to the verification backend and other parts of SBV. If you elaborate a bit more on what exactly is the issue with Frama-C, perhaps we can come up with an alternative solution.

Please do test the changes I just pushed and let me know if anything breaks!

[GAJaloyan]

I made the tests, and it works quite well (compCert manages to compile everything).

Some other issues :

• Signed casts from Int32 to Int64 (for example) : is there an easy way to do that ? We only have to extend the number with its first byte (LE convention).
• ShiftL, ShitR with symbolic values : it seems that it is already implemented in the Operation.hs , but it has to be transfered in the file Model.hs (instead of prompting an error). -- | Generalization of 'svShl', where the shift-amount is symbolic. -- The shift amount must be an unsigned quantity. svShiftLeft :: SVal -> SVal -> SVal
• LOr/LAnd : Actually bitwise works on the value-analysis plugin of frama-c, but not on wp plugin (weakest liberal precondition calculation). The fact is that the typing makes impossible to write something like 1 || 98, we can only have logical operation on booleans. This means that proving a theorem on a bitwise logical expression on booleans implies the same result when replacing all operators with their lazy logical variants (which is not the case if we allow logical for non boolean, 2 & 1 = 0 --> false whereas 2 && 1 != 0 --> true). The fact is that when you send to the model checker a lazy operator (&&& or |||), it automatically converts it in bitwise, and then keeps it bitwise. The idea would be to change it to logical after getting out of the model checker, which will not affect its soundness, but only its completeness (raise false alarms in case of a || bottom, whereas in the reality it will not crash). Of course, this is only valid if there is a strong type system, preventing the use of logical operators on non boolean types.

[LeventErkok]

• Signed conversions. There's the Splittable class; but it only supports unsigned conversions. There's no simple way to do signed-up/down converts currently; especially not one that'll generate good C code. Please file a separate ticket for this and I'll see if that can be added.
• SBV already exports sbvShiftLeft and sbvShiftRight that allows for variable length shifts. The issue is that these will both generate "correct" but rather terrible C code. (Try it!) That's why I pointed out this example earlier: https://hackage.haskell.org/package/sbv-4.4/docs/src/Data-SBV-Examples-CodeGeneration-Uninterpreted.html#shiftLeft Please take a look at that and let me know if that doesn't do the trick for you.
• LOr/LAnd: Can you make a separate ticket for this as well. I think there might be an easy solution, based in your description; but I need to think about it a bit.

[GAJaloyan]

• I managed to cast from Word16 to Int32 using signCast, but I do not think that it is a very beautiful way to do it. Anyway, I'll open an other ticket about it, but it's not urgent.
• I tried some shiftL, shiftR. Even if the code generated is ugly (only because of the static keyword), it's ok since frama-c does not have any problem proving it :

/@ assigns \nothing; ensures \result == (((1) << (queue_0[ptr_0]))); / SWord64 observer_hist(const SWord64 *queue_0, const SWord32 ptr_0) {UglyFunction ...}

[value] computing for function observer_hist <- updateObservers <- step. Called from driver.c:42. observer_hist.c:17:[value] Function observer_hist: postcondition got status valid. [value] Recording results for observer_hist [value] Done for function observer_hist

• I'll open a new ticket for that.

[LeventErkok]

@Varmin

Earlier you said:

Addendum : I tried the floating operations, but they work only on 
constants as specified in BitVectors/Model.hs (ACSL is not able to handle them anyway).
Is there a way to force the compiling of the expression (meamning that it will produce a
C code for it), instead of crashing in case of a non constant operation?

I'm not sure what this is referring to? Can you give an example? All float-expressions should be compiled to C just fine.

Better yet, please open a new ticket so we can track it precisely what the problem is.

[GAJaloyan]

I created a new ticket about it.

But still talking about ACSL : is there a way to add a comment inside the code of a function ? I thought of adding a unary (or binary, depending on how you see it) operator named label (String -> SBV a -> SBV a), that will add a comment inside an expression, just to know where it finishes in the code after compilation.

[LeventErkok]

Due to lazy evaluation of Haskell; such a "labeling" mechanism is unlikely to be reliable. But we can surely add something that can give you that flavor. Please open a new ticket for that and we'll track it separately.

[LeventErkok]

@Varmin I think all the issues raised in this ticket are either resolved, or have their own tickets. Am I correct? If so, please close this one.