search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
819 stars 258 forks source link

Generating GOTO-programs as front-end to other tool #8309

Open echancrure opened 3 months ago

echancrure commented 3 months ago

I am looking to use GOTO-Programs, as hopefully generated by GOTO-CL, as a front-end for my testing tool, and I am wondering what the best way forward is. Looking at two other projects which did, this did not help: 2LS is an offshoot rather than a sperate project, and Pinaka's code is not open-source. My idea would be to parse GOTO-programs in text format into a format suitable for my tool (Prolog clauses). I already have a parser for generic C that I was hoping to reuse on goto-programs.

Here is what I have tried so far using CBMC version 5.95.1 for Windows:

  1. using goto-cl on the command line: but I could only generate a GOTO binary
  2. using cbmc --show-goto-functions mult.c (as per the documentation on goto-programs) but:
    • the output program is different than documented
    • the output is more removed from C (my parser would need serious rework) than the documented example in https://diffblue.github.io/cbmc/group__goto-programs.html ( e.g. use of := instead of = for assignment)
    • the exact syntax of GOTO-programs is unclear to me
    • it also generates binaries, which I don't need.

I understand, reading around this repository, that it appears that the preferred way of interacting with CBMC is via API calls, but I think this would be quite harder as an outsider to the CBMC project (as I am a part-time team of one person) than simply parsing simple C from goto-cc output.

I find the idea of using goto-programs as a front end very attractive for C-based tools, but at the moment I don't see how to proceed.

To simplify, I have 2 questions:

  1. is there a way to only generate goto-programs that are close to C in text form so that I can reuse my C parser today?
  2. if not, is there a detailed tutorial showing how to manipulate the internal AST to generate tailored output, that I can master in a week?

I am open to other suggestions for handling the messy world of C.

Many thanks, Dr Chris Meudec http://www.echancrure.eu/

kroening commented 3 months ago

Would the JSON serialisation useful for you?

echancrure commented 3 months ago

Potentially, although it would be far removed from parsing C, I don't have examples of outputs or know how to generate one.

Perhaps "C Intermediate Language" https://people.eecs.berkeley.edu/~necula/cil/ is more what I need.