Feature request - C compiler

[jeremy-rutman]

We'd like to be able to use cryptol to generate C that can be directly used on microcontrollers on which Rust is not yet implemented - is there a cryptol->C compiler in the works?

[kiniry]

Such a compiler already exists. It is largely not part of our public release of Cryptol. We have used to it generate systems and components for embedded systems development. An example of its use is found in the public HARDENS project, which was developed for the Nuclear Regulatory Commission.

On Thu, Mar 7, 2024 at 10:08 AM jeremy rutman @.***> wrote:

We'd like to be able to use cryptol to generate C that can be directly used on microcontrollers on which Rust is not yet implemented - is there a cryptol->C compiler in the works?

— Reply to this email directly, view it on GitHub https://github.com/GaloisInc/cryptol-compiler/issues/42, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADU5P75SK2FOEXCFABFWKTYXCUJBAVCNFSM6AAAAABELPF7V6VHI2DSMVQWIX3LMV43ASLTON2WKOZSGE3TINBVGM3DAMY . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[weaversa]

There is also a Cryptol -> C generation capability in SAW. It is very easy to use, generates a test bench along w/ the C, and works well for individual functions.

$ saw
sawscript> enable_experimental
sawscript> :h codegen
Description
-----------

    codegen : String -> [String] -> String -> Term -> TopLevel ()

Generate straight-line C code for the given term using SBV.

First argument is directory path ("" for stdout) for generating files.
Second argument is the list of function names to leave uninterpreted.
Third argument is C function name.
Fourth argument is the term to generate code for. It must be a
first-order function whose arguments and result are all of type
Bit, [8], [16], [32], or [64].

sawscript> codegen "directory" [] "functionNameInC" {{ \(x : [32]) -> x + 1 }}
Creating directory "directory"..
Generating: "directory/Makefile"..
Generating: "directory/functionNameInC.h"..
Generating: "directory/functionNameInC_driver.c"..
Generating: "directory/functionNameInC.c"..
Done.
sawscript> :q
$ make -C directory
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC.c -o functionNameInC.o
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC_driver.c -o functionNameInC_driver.o
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer functionNameInC.o functionNameInC_driver.o -o functionNameInC_driver
$ directory/functionNameInC_driver
functionNameInC(0x772a5561UL) = 0x772a5562UL

[kiniry]

And direct LLVM generation as well, in another private project/branch. And JVM generation...

On Thu, Mar 7, 2024 at 10:46 AM weaversa @.***> wrote:

There is also a Cryptol -> C generation capability in SAW https://github.com/GaloisInc/saw-script. It is very easy to use, generates a test bench along w/ the C, and works well for individual functions.

$ saw sawscript> enable_experimental sawscript> :h codegen Description

codegen : String -> [String] -> String -> Term -> TopLevel ()

Generate straight-line C code for the given term using SBV.

First argument is directory path ("" for stdout) for generating files. Second argument is the list of function names to leave uninterpreted. Third argument is C function name. Fourth argument is the term to generate code for. It must be a first-order function whose arguments and result are all of type Bit, [8], [16], [32], or [64].

sawscript> codegen "directory" [] "functionNameInC" {{ (x : [32]) -> x + 1 }} Creating directory "directory".. Generating: "directory/Makefile".. Generating: "directory/functionNameInC.h".. Generating: "directory/functionNameInC_driver.c".. Generating: "directory/functionNameInC.c".. Done. sawscript> :q $ make -C directory cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC.c -o functionNameInC.o cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC_driver.c -o functionNameInC_driver.o cc -Wall -O3 -DNDEBUG -fomit-frame-pointer functionNameInC.o functionNameInC_driver.o -o functionNameInC_driver $ directory/functionNameInC_driver functionNameInC(0x772a5561UL) = 0x772a5562UL

— Reply to this email directly, view it on GitHub https://github.com/GaloisInc/cryptol-compiler/issues/42#issuecomment-1984204290, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADU5PZ73EDVQAGHLDZLTZDYXCYXZAVCNFSM6AAAAABELPF7V6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSOBUGIYDIMRZGA . You are receiving this because you commented.Message ID: @.***>

[jeremy-rutman]

Thanks all, very helpful. I must have missed references to C generation in the docs.

[jeremy-rutman]

Such a compiler already exists. It is largely not part of our public release of Cryptol. We have used to it generate systems and components for embedded systems development. An example of its use is found in the public HARDENS project, which was developed for the Nuclear Regulatory Commission.

I've gone through a lot of the HARDENS documentation and can't seem to find a cryptol->C section, if possible can you let me know what the compiler or codegenerator name is, or any other pointer to the right place? Thanks - JR

[jeremy-rutman]

There is also a Cryptol -> C generation capability in SAW. It is very easy to use, generates a test bench along w/ the C, and works well for individual functions.

$ saw
sawscript> enable_experimental
sawscript> :h codegen
Description
-----------

    codegen : String -> [String] -> String -> Term -> TopLevel ()

Generate straight-line C code for the given term using SBV.

First argument is directory path ("" for stdout) for generating files.
Second argument is the list of function names to leave uninterpreted.
Third argument is C function name.
Fourth argument is the term to generate code for. It must be a
first-order function whose arguments and result are all of type
Bit, [8], [16], [32], or [64].

sawscript> codegen "directory" [] "functionNameInC" {{ \(x : [32]) -> x + 1 }}
Creating directory "directory"..
Generating: "directory/Makefile"..
Generating: "directory/functionNameInC.h"..
Generating: "directory/functionNameInC_driver.c"..
Generating: "directory/functionNameInC.c"..
Done.
sawscript> :q
$ make -C directory
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC.c -o functionNameInC.o
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer -c functionNameInC_driver.c -o functionNameInC_driver.o
cc -Wall -O3 -DNDEBUG -fomit-frame-pointer functionNameInC.o functionNameInC_driver.o -o functionNameInC_driver
$ directory/functionNameInC_driver
functionNameInC(0x772a5561UL) = 0x772a5562UL

This is great - I didn't see the codegen on first look at SAW. Is there a way to import a .cry file into SAW such that I could for instance generate the C equivalent of the DES.cry script?

[weaversa]

This is great - I didn't see the codegen on first look at SAW. Is there a way to import a .cry file into SAW such that I could for instance generate the C equivalent of the DES.cry script?

Yep! It's just import "path\to\DES.cry";

[jeremy-rutman]

I tried importing DES and doing codegen from DES.encrypt but hit a 'not yet supported':

sawscript> import "DES.cry"
sawscript> codegen "des_c" [] "des_c" {{DES.encrypt}}

SBV->C: Not yet supported: join with ((SWord 1,s6),(SWord 1,s9))
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Compilers/C.hs:108:11 in sbv-10.2-6c0cf9c528cdb45a38ec91ea9af248f20680acc36f40bf77ed55529a9baf928e:Data.SBV.Compilers.C

Any help getting encrypt/decrypt C code from any cryptol example would be greatly appreciated.

[andrew-bivin]

@jeremy-rutman You'll hear from other folks more officially, but getting you the instructions on the proof of concept for Cryptol -> C for AES via the libvcrypt repo:

1. Clone https://github.com/GaloisInc/libvcrypt
2. Build saw if necessary
3. cd Ciphers/Symmetric/AES
4. saw codegen.saw

[jeremy-rutman]

Yes I actually already tried this and it indeed works to allow saw to create code for AES encrypt and decrypt. The encrypt compiles and runs fine but the decrypt hits an internal compiler error (for gcc 13.2.0) which I'm trying to hunt down now; I put a gcc bugreport at https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114855. Since clang does seem able to compile the decrypt it looks like this is a bona fide gcc bug. I can (probably) continue on my way using the saw-generated code using clang, thanks everyone for all the help! ... update, the matlab 'mex' compiler which it turns out is the one we're actually using, compiles the cryptol code fine.