This presentation introduces C2Priscal, an automated tool developed to translate C source code into PlusCal specifications for formal model checking using TLA+ and TLC. Developed as part of an internship at Asteros Technologies, the tool aims to verify safety properties on simple C code, particularly for embedded systems like microkernels, thereby reducing the need for exhaustive manual testing. The tool leverages the Frama-C platform to parse C code into a 'Seal' intermediate representation, which is then translated into a custom PlusCal-like intermediate representation before generating the final PlusCal and TLC configuration files. Key aspects of the translation include representing C variables as pointers, complex data structures (arrays, structs) as sequences and records in memory stacks (mem, my_stack, wet), and handling control flow structures like loops and gotos using PlusCal constructs facilitated by the Seal representation. While the tool is currently incomplete, an experimental application on an older version of a scheduler's source code successfully found a known bug using TLC model checking, demonstrating the potential of this approach for automating verification. Limitations include verbosity of generated code, handling complex pointer arithmetic, and managing state space explosion due to fine-grained transitions, but future work aims to incorporate multi-threading and improve the translation process.
Automated Translation of C to PlusCal for Model Checking
0:02 Project Goal: The presentation is about translating C code to PlusCal for model checking safety properties on source code, developed at Asteros Technologies.
0:24 Context: The project is part of a student internship aiming to use TLA+ to verify real-time synchronous algorithms of Asteros Technologies' microkernel, specifically experimenting with verifying directly from C source code.
0:46 Motivation: Automating translation from simple C code to TLA+ (later shifted to PlusCal) was motivated by previous PhD work and the concise nature of the kernel scheduler code.
0:57 Objective: The primary objective is to automate C program translation into PlusCal to facilitate verification.
0:08 C2Priscal Tool: The tool, called C2Priscal, is built using Frama-C (an OCaml-based C analysis platform) to preprocess C code into a 'Seal' representation.
0:36 Memory Representation: The tool represents memory using sequences in PlusCal.
0:42 C to PlusCal Translation: C functions are translated to PlusCal procedures.
0:03 Memory Locations: Three memory locations are used: mem (shared, for global variables), my_stack (for local variables, simulating a stack), and wet (for return values). This simulates a simplified C interpreter in PlusCal.
10:34 Variable Representation: C variables are represented as pointers (records with location, frame pointer, and offset) to values in the memory stacks. Macros (load, store, wait_at_value, decl) are defined for memory access.
13:46 Example Translation: A simple C function is shown being translated into a PlusCal procedure demonstrating the use of pointers and memory access macros.
16:11 Global Variable Initialization: Global variables are initialized in a separate PlusCal process, controlled by a global flag to ensure initialization completes before other processes start. This design anticipates potential future multi-threaded C code translation.
18:06 Seal Representation Utility: The Seal representation simplifies translation by transforming loops into while(true) with break levels and goto statements, which are directly supported in PlusCal. It also separates side effects into distinct statements.
20:22 Complex Data Structures: Arrays are represented as sequences and structs as records in PlusCal, allowing for direct translation when sizes are fixed (static context).
21:30 Array Initialization: A PlusCal procedure initializes arrays with undefined values based on their size.
22:13 Pointer Arithmetic: The pointer representation simplifies pointer arithmetic (adding/subtracting integers or other pointers) because all data types have a logical size of one in the memory stacks.
23:49 Memory Management Refinement: An improved pointer representation is introduced to handle addresses of struct fields or array elements and complex pointer expressions (e.g., **x), using nested pointer records and references (field name or index).
27:27 Homogenized Access: The new pointer representation allows using the same store macro for array element or struct field updates, simplifying the translation.
28:28 Updated Macros:load and store macros are updated to recursively handle the new nested pointer representation, tracing back to the base pointer in memory and then accessing the referenced element (field or index) using TLA+ operators.
31:15 Experimental Results: The tool is incomplete due to the internship duration but was used to translate parts of the scheduler code.
31:24 Bug Finding: An end-written (manual) translation of the scheduler found a known bug using TLC model checking in approximately 45 minutes on a 10-core processor. The environment used was intuitive.
33:13 Limitations: The generated PlusCal is long and verbose, making it hard to read and write properties. Arbitrary abstractions for hardware specifics lack proximity to source code. The tool has internal limitations like potential state space explosion from levels added per transition, duplicated label names from Frama-C Seal, incomplete pointer handling, and lack of support for certain C syntax (e.g., switch).
34:53 Perspectives: Future evolutions include handling multi-threaded C programs (as distinct PlusCal processes) and encouraging contributions as the project is open source.
35:19 Conclusion: The project was an experimental approach to automating translation, showing promising results despite limitations.
35:51 Future Exploration: Ideas for future work include using TLA+ proof system (TLAPS) for formal proofs on translated code, trying different model checkers like Apalache, and formally showing that the translated specification refines an abstract specification.
36:47 Acknowledgements: The presenter thanks Asteros Technologies, particularly supervisors Emanuel and Amira.