The C programming language is widely used in safety-critical software systems. With its large appliance and increasing complexity, the need of ensuring the correctness of C codes emerged. This paper presents Ceagle , a fully automated program verifier for finding assertion violations in C programs. It is decent in both accuracy and efficiency by using a semantically equivalent program model language that is specifically designed for C program, together with various optimizations that make the satisfiability checking faster and memoryfriendly. More specifically, Ceagle uses LLVM clang as front-end parser, an extended labeled transition system as program model, and Z3 SMT solver as the back-end satisfiability checker. Ceagle is designed to be fully automatic and requires no user interaction as long as the assertions are provided. For evaluation, we compare Ceagle with existing C program verifiers based on open benchmarks. Ceagle outperforms others in terms of accuracy, and time and memory consumption.
Many safety critical software systems use C programming language, and the verification
of safety properties of C programs are widely adopted to ensure the safety of the whole
software system [
In fact, an ideal verification tool is supposed to be fast, memory friendly and accurate, but it is not easy to achieve all of them in real cases. For example, a verification tool that is very accurate may suffer from low performance, and needs a long time and huge memory to get a relative complete and sound result.
Except for the performance and accuracy, the usability of the verification tool is another important issue. Users prefer verification tools that require less user interaction than those require manual mathematical proof injection or even sophisticated formal verification knowledge background.
In this paper, we propose a novel verification tool Ceagle to get a better balance between the performance and accuracy, and needs less interaction from users. It is comparatively accurate and efficient by using a semantically equivalent program model language that is specifically designed for C programs, together with various optimizations that make the satisfiability checking faster. The program model language extends the original labeled transition system (LTS) with more variable types, C style statements, and built-in functions. The extended labeled transition system (ELTS) inherits the inner property of traditional LTS that is suitable for the implementation of various model checking algorithms. Based on the ELTS, several optimizations are performed during C programs parsing, ELTS construction and ELTS analysis to make Ceagle faster and more memory friendly than other C verification tools.
ELTS Counterexample clang
LLVM IR ir2elts
ELTS core C
C Counterexample
SMT SMT Model z3
The overall structure of Ceagle is shown in Fig.1. Ceagle contains four components: clang, ir2elts, core, and z3. The C program is firstly parsed by LLVM clang, yielding the LLVM IR program. Then, the component ir2elts translates the generated LLVM IR program to the program model ELTS. Finally, the component core constructs SMT constraints from ELTS, and inputs them into the component z3 for verification. If the safety property is not satisfied, the C counterexample will be generated and presented automatically by the implemented trace-back engine. During the whole procedure, the program intermediate representation LLVM IR and program model ELTS play important roles in source-level and model-level optimizations, respectively.
All model translation and construction are accomplished automatically, the user just needs to input the C program and corresponding safety property assertions. It is easy to use and does not need complex interactions or formal verification knowledge background. For evaluation, we compare Ceagle with existing C program verifiers based on the benchmarks, and Ceagle uses about 20% memory and time of CBMC to acquire almost the same accuracy, and improves the accuracy of CPAchecker for 25%. 2
An intermediate program model ELTS is designed to represent the C program for optimized verification. Formally, an ELTS model S is a five tuple (L; l0; V; V0; T ) where: – L is a finite non-empty set of locations; – l0 is the location of initial basic block; – V is a finite non-empty set of variables ranging over V, where V is the (possible infinite) set of values of V ; – V0 is the set of initial values of V ; – T L V V L is a finite non-empty set of transitions, a transition t = (li; Vi; Vj ; lj ) 2 T can also be denoted as (li; Vi) ! (lj ; Vj ), li and lj are called f rom and to locations, respectively.
ELTS is extended from the traditional labeled transition system to support all kinds of operations and types of C programs. For example, the built-in floating point functions such as fpclassifyf and isnanf contained in math.h are reserved in the element T of ELTS and will be translated to corresponding SMT constraints later during satisfiability checking. Details of ELTS can be referred to the website1. 3
During the last decades, there are approaches of assuring quality of programs by
modeling and formal verification [
As presented in Fig. 1, Ceagle contains four components: clang, ir2elts, core, and z3,
where clang [
LLVM clang : This component is used to translate C to LLVM IR. A program is firstly parsed by LLVM clang, yielding the LLVM IR program with debug information, the debug information will be used in C counterexample generation.
Translator ir2elts : This component translates LLVM IR program to the ELTS model. Each basic block in LLVM IR program is translated into the corresponding transition in an ELTS model with four steps: (i) the name of f rom (to) location in ELTS model is the label value of the current (successor) basic block in LLVM IR program; (ii) the guard condition of the transition in ELTS model is translated from the goto-condition of the current basic block in LLVM IR program; (iii) the body of the current basic block is copied as-is to preserve full LLVM IR semantics, except that LLVM IR instructions are translated into ELTS statements; (iv) assertion calls in LLVM IR program are translated into guarded transitions to error locations. 1 http://sts.thss.tsinghua.edu.cn/ceagle Formalizer core : This component constructs SMT constraints based on the ELTS model and assertion. It performs reachability analysis of the translated error locations via a depth-first search (DFS) on the ELTS model. Once DFS reaches an error location, it constructs an SMT trace constraint containing those transitions from the initial location to current error label. It returns “TRUE” if error location is not reachable in ELTS, otherwise, it returns “FALSE” along with an ELTS counterexample, which is an ELTS trace that starts from the initial location to error location. Another function of this component is to convert the ELTS counterexample back to the C counterexample. The reverse mapping information from ELTS model to LLVM IR program is preserved by ir2elts when it translates LLVM IR program to ELTS model, and the reverse mapping information from LLVM IR program to C source code is preserved by clang via debug information stored in LLVM IR program.
Solver z3 : This component checks the satisfiability of the formalized constraint, and infers violations of assertions by the following rules: (i) if the result is sat together with an SMT model, it means there exists an assignment of variables that can make the program executes to error label, thus proves an assertion violation; (ii) if the result is unsat, it means the current trace is safe, the DFS continues; (iii) if all traces are checked to be unsat, the program is proved to be safe. 4.2
There are two main reasons that bring up the state space explosion problem and prevent a verifier from analyzing the C program efficiently: structural complexity and a large number of variables. We aim at reducing both of them through LLVM IR program, ELTS model, and formalization optimizations.
LLVM IR program optimization : We observe that there are basic blocks in the LLVM
IR that are not reachable from the program entry, which can be removed when being
translated to ELTS. There are also set of basic blocks that have no conditional jumps
and can be merged into one large basic block, thus helps reducing verification state
space. On the other hand, an LLVM IR program is constructed in static single
assignment (SSA) form [
ELTS model optimization : In the ELTS model level, a depth-first search (DFS) is carried out to help to generate SMT constraints of all paths. Optimizations on ELTS model are performed to reduce the search space as follows. First, more variables are trimmed away through methods of constant propagation, temporary variables are eliminated, and locations that are not reachable to error labels are deleted, thus reduces nodes the DFS has to visit. Second, we perform optimization during the DFS search, where variables from different transitions are annotated with a sequence number according to the index of the transition in the ELTS trace, which makes it easier to construct counterexamples after satisfiability checking.
Formalization optimization : A program usually contains multiple kinds of types, such
as boolean, integer, and floating point, which brings several challenges to construct the
constraints in a precise and efficient way. Traditional methods solve mixed-type
expressions and type conversion problems by using precise memory model [
The expression is consists of variables, constants, and operators, and we encode an expression as a directed acyclic graph, in which non-leaf nodes are operators, their children are their operands, and the leaves are labeled with variables or constants. For every expression e, we record two types: “intrinsic” type tyi(e) and “to-be” type tytobe(e). The intrinsic type is the expression evaluated to be, and the “to-be” type is the expression that should be converted to be when the expression is participating in parental expressions. The “to-be” type is inferred lazily, and integers and floating points are evaluated to be bit-vector “to-be” type when the operator is bit-precise. In this way, variables that are not necessarily to be analyzed bit-precisely can keep being arithmetic, thus reduces constraint satisfiability overhead of the back end SMT solver. 5
Experiment setup : We compared Ceagle with the most widely used and recently
developed C verifiers CBMC 5.2 and CPAchecker 1.4, in terms of the accuracy, time and
memory consumption. They are tested on the set of benchmarks from the software
verification competition held at TACAS [
More specifically, we conducted the experiments on the 81 files in the Floats benchmark set, with a total of approx. 5K lines of code. The experiments are performed on a machine with a 3.4 GHz 64-bit Quad Core CPU (Intel i7-4770) processor and 32GB of memory, running an Ubuntu 14.04 with a 64-bit Linux kernel 4.2.0. We set a 15GB memory limit and a 900s timeout for the analysis of each subject.
Verification result : The experiments for the three tools are summarized in Table 1. In the results table, correct negative means the file is true (i.e., negative, assertions are not violated) and the tool reported true, correct positive means the file is false (i.e., positive, assertions are violated) and the tool reported false, incorrect negative means the file is false but the tool reported true (usually means an unsound tool), incorrect positive means the file is true but the tool reported false (i.e., a false alarm, usually means an incomplete tool). Ceagle reported 77 correct and 4 unknown results for total 81 benchmarks, CBMC reported 78 correct and 3 unknown, and CPAchecker reported 56 correct, 1 incorrect, 6 unknown, and 18 timeout results. The correctness rate is computed by the division of the number of correct files and the number of total files (81), so the three tools have correctness rates of 95.06%, 96.30%, and 69.15%, respectively. Ceagle uses about 10%-20% memory and time consumption of CBMC and CPAchecker, but acquires almost the same accuracy (just one more unknown file) of CBMC and improves the accuracy of CPAchecker for 25%. It is reasonable to draw the conclusion that Ceagle is efficient in both time and memory usage while maintaining a high correctness rate. More details about efficiency are analyzed and illustrated as follows.
We presented both the time and memory consumption in the third and fourth row of Table 1. Ceagle is about 5.5X faster than CBMC and 5X faster than CPAchecker on arbitrary files. Note that Ceagle is a little bit slower than CPAchecker if only counting correct results, and it would be much faster than CPAchecker when including those incorrect and timeout results. Ceagle uses about 80% lesser memory than CBMC and
Ceagle 1.0 CBMC 5.2 CPAchecker 1.4 Number of correct files 77 78 56 Correct negatives 59 56 35 Correct positives 18 22 21 Number of incorrect files 0 0 1 Incorrect negatives 0 0 0 Incorrect positives 0 0 1 Unkowns 4 3 6 Timouts 0 0 18 Correctness rate (%) 95.06 96.30 69.14 Total time (s) 3700 21000 19000 Total time of correct files (s) 3700 18000 2500 Time per file (s) 45.68 259.26 234.57 Timer per correct file (s) 48.05 230.77 44.64 Time ratio of per file (%) 100.00 567.56 513.51 Time ratio of per correct file (%) 100.00 480.27 92.90 Total memory (MB) 2900 15000 31000 Total memory of correct files (MB) 2900 13000 17000 Memory per file (MB) 35.80 185.19 382.72 Memory per correct file (MB) 37.66 166.67 303.57 Memory ratio of per file (%) 100.00 517.29 10069.05
Memory ratio of per correct file (%) 100.00 442.57 806.08 90% lesser memory than CPAchecker on arbitrary files. This is because the optimizations at different levels (LLVM IR program, ELTS model, and constraint formalization) help to reduce much verification overhead, thus reduces time and memory usage.
For the unknown and timeout result files, Ceagle output 4 unknown due to its lacking full support of arrays and some internal bugs on handling high order multiplications of floating points. CBMC output 3 unknown and crashed without any prompts. CPAchecker reported 6 unknown and 18 timeouts. The 6 unknown files are because of incomplete analysis. The 18 timeout files are all true files, and it is because when the value analysis algorithm of CPAchecker found no counterexample, the predicate analysis algorithm would be used, which consumed a lot of time but still could not prove true for these files. 6
In this paper, we presented the C program verifier Ceagle to check assertion violations of C programs. It uses LLVM clang as front-end parser, an extended labeled transition system as program model, and Z3 SMT solver as the back-end satisfiability checker. Several optimization techniques during the three steps are designed and implemented to reduce the memory and time consumption. Except for those experiments on benchmarks, we have applied Ceagle to verify the core optimization algorithm which has 17k LOC of C code of the real train energy efficiency control software for smart railway transportation. Several safety assertions are inserted in the code to check its safety, and an over speed bug in the code is detected. Our future work mainly includes extending the scalability of Ceagle to support more advanced features such as struct and dynamic memory allocation of C programming language.