c-semantics

c-semantics copied to clipboard

C often finds usages on systems that lack the ability to run anything else. Running K on such systems is often not an option. There can be many reasons behind this: for instance, lack of a compatible JVM, or just lack of resources to run a rather large application like K (I haven't tried running K on a small system like the Raspberry Pi, but it'll be interesting to see what the performance is like). C code running on such systems is often available though, and it'll be interesting to see whether we can run the code on K running on a completely separate system. Since the code would not be executing on the machine itself, we'd mostly be lacking the ability to perform any sort of concrete execution. However, symbolic execution of the code may be possible. @andreistefanescu and I were able to verify several programs withing the SV-COMP testbench by performing symbolic execution. The programs in the testbench however, were much simpler than the kind we'd encounter on embedded systems. Furthermore, the code, apart from having C, may have assembly as well. The purpose of opening this issue to spur a discussion on this topic.

So, the OCAML backend is capable of running programs on any system that ocamlopt can compile to, which last I checked included Android and iOS. The larger issue is that many embedded systems use specific architectures that are distinct from amd64 and ARM, and those architectures are likely going to be quite hard to support in that context. But one of our plans as a company is to investigate the practice of running programs as an interaction between K running on a PC, and the native code running on the target platform, while communicating over a network.