search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
51 stars 28 forks source link

[CN] Support memcpy_proxy and memcmp_proxy #294

Open dc-mak opened 4 months ago

dc-mak commented 4 months ago

Specifications from here are sufficient for the CN VIP test cases but not necessarily complete.

https://github.com/rems-project/cerberus/blob/cn-vip-testing/tests/cn_vip_testsuite/cn_lemmas.h

Likely a few days work.

thatplguy commented 3 months ago

@dc-mak can you add a "blocking others" label to this issue? I don't seem to have permissions to add labels. This is blocking TA2 from porting the next OpenSUT component (see this OpenSUT issue).

Any sense how far out the VIP work is from being merged into main – days, weeks, months?

dc-mak commented 3 months ago

I have a work-around for this if that helps: https://github.com/rems-project/cerberus/tree/master/tests/cn_vip_testsuite VIP work is on the order of weeks away (single digits, it's close to the top of the stack) - also, it's not just using memcpy/memcmp, but converting C values to/from bytes. Both can be worked around, but the latter is tedious until automated.

samcowger commented 3 months ago

Apologies for what might be a digression, but I was recently tripped up by an error about a missing _proxy function and I wasn't sure what to make of it. It seems like CN (or Cerberus, perhaps) tries to substitute f_proxy for any f in some particular set/environment, and completes its analysis according to f_proxy's spec/definition instead of f's. Further, it seems like this behavior is expected and relatively well-defined. My questions are:

Also, if there's publicly-available reference material on this behavior, I did not find it, and would appreciate a pointer to it!

dc-mak commented 3 months ago

No worries, and you are basically right. So the reference for Cerberus related things is usually: https://www.repository.cam.ac.uk/items/ea7fff60-301b-450f-afbc-bd82a2704989

However, proxies are not really mentioned in there, so my best guess is that they are an engineering features, a Cerberus way of expressing in its core language, C functions which need special handling of some sort. Think of them like C standard (library) primitives / "compiler intrinsics". Cerberus wants calls to memcmp and memcpy not to defer to the "implementation", but to defer to the abstract memory model, so it replaces calls to them with calls to the proxies.

You can ➜ cerberus git:(master) grep "proc.*_proxy" -R . --exclude-dir=_build to find them all (they're in runtime/libcore/std.core or runtime/libcore/std_inner_arg_temps.core).

@kmemarian Anything else to add?

As for CN, we add support for proxies on a case-by-case basis as a result. They will be supported as in-built primitives essentially.

samcowger commented 3 months ago

Thanks, that makes sense. Based on my experience, and the behavior described in https://github.com/GaloisInc/VERSE-Toolchain/issues/103, I'm guessing I need to somehow manually include the models defined in runtime/libcore/std.core if I want to refer to them in a CN spec. Is there documentation on how to do that?

dc-mak commented 3 months ago

I'm not sure I understand. I'll be implementing specs for memcpy/memcmp soon. What are you trying to do? Maybe have a look in here in the meantime? https://github.com/rems-project/cerberus/tree/master/tests/cn_vip_testsuite

samcowger commented 3 months ago

At a high level, I guess I want to know if I have any recourse when seeing a message like "Unknown function f_proxy", e.g. whether there's some extra step I need to take to ensure CN knows where to look for a spec for f_proxy. It seems like for now I have no recourse, because no specs exist yet, but when they do, I would need to #include the file in which they're defined.

I think I was confused about what exactly runtime/libcore/std.core defines, because I thought that manually pointing CN to it would resolve this issue, but I guess its definitions don't constitute "specs" proper.

dc-mak commented 3 months ago

Correct. One very useful (long term) thing would be to come up with a spec for the function, and making an issue/PR with that because that's most of the challenge. Once you have that, adding it to the type-checker is straightforward enough. You can use some preprocessor shenanigans to to #ifdef CN some specs (and renamings) to experiment.