Consider flag/config file for specifying impl-defined behaviour

[yav]

Testing the following example fails with a violation of the ensures clause.
It however works if we use explicit unsigned char or signed char.

It looks like the error might be a disagreement between the generator and the execution on the sign-edness of char (perhaps one is assume that is signed and the other that it is unsgined?)

int f(char x, char y)                                                               
/*@                                                                                 
requires x < y;                                                                  
ensures return == 1i32;                                                          
@*/                                                                              
{                                                                                
  return x < y;                                                                  
}     

cn --version
git-368d51a1f [2024-11-05 10:05:01 -0500]

[ZippeyKeys12]

From my understanding CN is parametric over things such as the signedness of chars and size of ints (thanks to Cerberus), so for runtime testing you'd need to ensure that its using the same model/config/whatever as the system you're running the tests or instrumentation on.

I don't know how that is done, perhaps @dc-mak or @cp526 can help.

This shows up in testing because the execution of the user's code follows their system's rules, but the executable spec generates code based on the CN types (u8 for char in this case). That's why the failure is in the postcondition, but it passes the precondition.

To see with just the instrumentation:

int f(char x, char y)
/*@
requires x < y;
ensures return == 1i32;
@*/
{
  return x < y;
}

int main() {
  f(100, -25);
}

The precondition is unsigned, due to CN converting char to u8.

/* EXECUTABLE CN PRECONDITION */
cn_bits_u8* x_cn = convert_to_cn_bits_u8(x);
cn_bits_u8* y_cn = convert_to_cn_bits_u8(y);
cn_assert(cn_bits_u8_lt(x_cn, y_cn));

[dc-mak]

The signed-ness of char is an implementation-defined detail. In CN, it's hard-coded to pKVM-friendly defaults here:

cerberus/backend/cn/bin/main.ml

Line 66 in 368d51a

Ocaml_implementation.set Ocaml_implementation.HafniumImpl.impl;

Though that doesn't say much about how to proceed.

[yav]

Perhaps we could add a flag or a configuration file to CN for specifying implementation defined behavior?

[cp526]

Cerberus's cerberus/ocaml_frontend/ocaml_implementation.ml defines a number of different implementation profiles; backend/cn/bin/main.ml picks Ocaml_implementation.HafniumImpl.impl; (which is good for pKVM. It would probably be easy to make this switchable.

It's not clear to me how this relates to let impl_name = "gcc_4.9.0_x86_64-apple-darwin10.8.0" in setup.ml. @kmemarian ?

[cp526]

If we make this switchable, we should check how normal cerberus does the same switching and mirror that.