Authors Basile Desloges Julien Signoles Kostyantyn Vorobyov
License CC-BY-SA-4.0
E-ACSL User Manual E-ACSL Plug-in Release 24.0 (Chromium) Julien Signoles, Basile Desloges and Kostyantyn Vorobyov This work is licensed under a Creative Commons “Attribution- ShareAlike 4.0 International” license. CEA-List, Université Paris-Saclay Software Safety and Security Lab ©2013-2021 CEA LIST CONTENTS Contents Foreword 7 1 Introduction 9 2 What the Plug-in Provides 11 2.1 Simple Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.1 Running E-ACSL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.1.2 Executing the generated code . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 E-ACSL Wrapper Script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.1 Standard Usage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.2 Customising Frama-C and Gcc Invocations . . . . . . . . . . . . . . 15 2.2.3 Verbosity Levels and Output Redirection . . . . . . . . . . . . . . . . 15 2.2.4 Architecture Dependency . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2.5 Documentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.3 Execution Environment of the Generated Code . . . . . . . . . . . . . . . . . 16 2.3.1 Runtime Errors in Annotations . . . . . . . . . . . . . . . . . . . . . . 17 2.3.2 Libc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3.3 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3.4 Memory-related Annotations . . . . . . . . . . . . . . . . . . . . . . . 19 2.3.5 Runtime Monitor Behavior . . . . . . . . . . . . . . . . . . . . . . . . 21 2.4 Additional Verifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.4.1 Format String Vulnerabilities . . . . . . . . . . . . . . . . . . . . . . . 23 2.4.2 Incorrect Usage of Libc Functions . . . . . . . . . . . . . . . . . . . . 24 2.5 Incomplete Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.5.1 Programs with no Main Function . . . . . . . . . . . . . . . . . . . . . 25 2.5.2 Undefined Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5.3 Providing a White List of Functions . . . . . . . . . . . . . . . . . . . 27 2.5.4 Partial Instrumentation (Experimental) . . . . . . . . . . . . . . . . 27 2.6 Combining E-ACSL with Other Plug-ins . . . . . . . . . . . . . . . . . . . . . 28 5 CONTENTS 2.7 Customization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.8 Verbosity Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.8.1 Verbosity Level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.8.2 Message Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 Known Limitations 33 3.1 Supported Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.1.1 Operating Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.1.2 Architectures and Runtime Library . . . . . . . . . . . . . . . . . . . . 33 3.2 Uninitialized Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.3 Incomplete Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.3.1 Programs without Main . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.3.2 Undefined Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.3.3 Incomplete Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.4 Recursive Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.5 Variadic Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.6 Function Pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.7 Requirements to Input Programs . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.7.1 E-ACSL Namespace . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.7.2 Memory Management Functions . . . . . . . . . . . . . . . . . . . . . 36 A Changes 37 Bibliography 41 Index 43 6 Foreword This is the user manual of the Frama-C plug-in E-ACSL1 . The contents of this document correspond to its version 24.0 compatible with 24.0 version of Frama-C [5, 8]. The devel- opment of the E-ACSL plug-in is still ongoing. Features described by this document may evolve in the future. Acknowledgements We gratefully thank the people who contributed to this document: Pierre-Loïc Garoche, Jens Gerlach, Florent Kirchner, Nikolaï Kosmatov, André Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot. 1 https://frama-c.com/fc-plugins/e-acsl.html 7 Chapter 1 Introduction Frama-C [5, 8] is a modular analysis framework for the C programming language which supports the ACSL specification language [2]. This manual documents the E-ACSL plug-in of Frama-C, version 24.0. The E-ACSL version you are using is indicated by the command frama-c -e-acsl-version. E-ACSL automatically translates an annotated C program into another program that fails at runtime if an annotation is violated. If no annotation is violated, the behavior of the new program is exactly the same as the one of the original program. E-ACSL translation brings several benefits. First, it allows a user to monitor C code and perform what is usually referred to as “runtime assertion checking” [4]1 . This is the primary goal of E-ACSL. Indirectly, in combination with the RTE plug-in [7] of Frama-C, this usage allows the user to detect undefined behaviors in its C code. Second, it allows to combine Frama-C and its existing analyzers with other C analyzers that do not natively understand the ACSL specification language. Third, the possibility to detect invalid annotations during a concrete execution may be very helpful while writing a correct specification of a given program, e.g. for later program proving. Finally, an executable specification makes it possible to check assertions that cannot be verified statically and thus to establish a link between runtime monitoring and static analysis tools such as Eva [3] or Wp [1]. Annotations used by the plug-in must be written in the E-ACSL specification language [13, 6] – a subset of ACSL. E-ACSL plug-in is still in a preliminary state: some parts of the E- ACSL specification language are not yet supported. Annotations supported by the plugin are described in a separate document [14]. It is worth noting that the annotations that aim to be dynamically verified are not necessarily hand-written, but may be automatically generated instead. That is for instance the case when checking the absence of undefined behaviors in combination with RTE, as mentionned in the previous paragraph. Using E-ACSL this way is therefore a fully automatic process. Many usages, including automatic usages, are described in companion research papers [11, 16, 15]. The E-ACSL plug-in is installed with Frama-C, but this manual does not explain how to install Frama-C. For installation instructions please refer to the INSTALL2 file in the Frama-C distribution. Furthermore, even though this manual provides examples, it is not a full comprehensive tutorial on Frama-C or E-ACSL. 1 In our context, “runtime annotation checking” would be more precise. 2 https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md 9 Chapter 2 What the Plug-in Provides This chapter is the core of this manual and describes how to use the E-ACSL plug-in. First, Section 2.1 shows how to run the plug-in on a toy example, compile the generated code with the Gcc compiler and detect invalid annotations at runtime. Further, Section 2.2 describes e-acsl-gcc.sh – a convenience wrapper script around Frama-C and Gcc. The aim of this script is to simplify instrumentation and compilation of the instrumented code. Section 2.3 gives additional details on the execution of the generated code. Next, Section 2.5 focuses on how to deal with incomplete programs, i.e. in which some functions are not defined or in which there are no main function. Section 2.6 explains how to combine the E-ACSL plug-in with other Frama-C plug-ins. Finally, Section 2.7 introduces how to customize the plug-in, and Section 2.8 details the verbosing policy of the plug-in. 2.1 Simple Example This section is a mini-tutorial which explains from scratch how to use the E-ACSL plug-in to detect whether an E-ACSL annotation is violated at runtime. 2.1.1 Running E-ACSL Consider the following program containing two E-ACSL assertions such that the first asser- tion is valid, whereas the second one is not. File first.i int main(void) { int x = 0; /∗@ assert x == 0; ∗/ /∗@ assert x == 1; ∗/ return 0; } Running E-ACSL on first.i consists of adding -e-acsl option to the Frama-C command line: $ frama-c -e-acsl first.i [kernel] Parsing first.i (no preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [e-acsl] translation done in project "e-acsl". 11 CHAPTER 2. WHAT THE PLUG-IN PROVIDES Even though first.i has already been pre-processed, E-ACSL first asks the Frama-C kernel to process and combine it against several header files provided by the E-ACSL plug- in. Further E-ACSL translates the annotated code into a new Frama-C project named e-acsl1 . By default, the option -e-acsl does nothing more. It is however possible to have a look at the generated code in the Frama-C GUI. This is also possible through the command line thanks to the kernel options -then-last and -print. The former switches to the last generated project, while the latter pretty prints the C code [5]: $ frama-c -e-acsl first.i -then-last -print [kernel] Parsing first.i (no preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [e-acsl] translation done in project "e-acsl". /* Generated by Frama-C */ #include "stddef.h" #include "stdio.h" struct __e_acsl_contract_t; typedef struct __e_acsl_contract_t __attribute__((FC_BUILTIN)) __e_acsl_contract_t; struct __e_acsl_mpz_struct { int _mp_alloc ; int _mp_size ; unsigned long *_mp_d ; }; typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct; typedef __e_acsl_mpz_struct ( __attribute__((FC_BUILTIN)) __e_acsl_mpz_t)[1]; struct __e_acsl_mpq_struct { __e_acsl_mpz_struct _mp_num ; __e_acsl_mpz_struct _mp_den ; }; typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct; typedef __e_acsl_mpq_struct ( __attribute__((FC_BUILTIN)) __e_acsl_mpq_t)[1]; typedef unsigned long __e_acsl_mp_bitcnt_t; /*@ requires pred != 0; assigns \nothing; */ __attribute__((FC_BUILTIN)) void __e_acsl_assert(int pred, char const *kind, char const *fct, char const *pred_txt, char const *file, int line); extern size_t __e_acsl_heap_allocation_size; extern size_t __e_acsl_heap_allocated_blocks; /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */ /*@ ghost extern int __e_acsl_init; */ long valid_nstring(char *s, long n, int wrtbl); long valid_nwstring(wchar_t *s, long n, int wrtbl); __inline static long valid_string__fc_inline(char *s, int wrtbl) 1 The notion of project is explained in Section 8.1 of the Frama-C user manual [5]. 12 2.1. SIMPLE EXAMPLE { long tmp; tmp = valid_nstring(s,(long)(-1),wrtbl); return tmp; } __inline static long valid_wstring__fc_inline(wchar_t *s, int wrtbl) { long tmp; tmp = valid_nwstring(s,(long)(-1),wrtbl); return tmp; } int main(void) { int __retres; int x = 0; __e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3); /*@ assert x == 0; */ ; __e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4); /*@ assert x == 1; */ ; __retres = 0; return __retres; } As you can see, the generated code contains additional type declarations, constant declara- tions and global ACSL annotations not present in the initial file first.i. They are part of the E-ACSL monitoring library. You can safely ignore them for now. The translated main function of first.i is displayed at the end. Before each E-ACSL annotation, a call to __e_acsl_assert has been added. __e_acsl_assert(x == 0,"Assertion","main","x == 0","first.i",3); /∗@ assert x == 0; ∗/ ; __e_acsl_assert(x == 1,"Assertion","main","x == 1","first.i",4); /∗@ assert x == 1; ∗/ ; Each call to __e_acsl_assert, function defined by the E-ACSL monitoring library, dynam- ically verifies the validity of the corresponding assertion. In other words, it checks that its first argument (here x == 0 or x == 1) is not equal to 0 and fails otherwise. The extra arguments are used to display error reports as shown in Section 2.1.2. 2.1.2 Executing the generated code Using -ocode Frama-C [5] option, the code generated by the E-ACSL plug-in can be redirected into a file as follows: $ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c Frama-C uses architecture-dependent configuration which affects sizes of integer types, en- dianness and potentially other features. It can be seen that the code generated from first.i (shown in the previous section) defines C type size_t as unsigned int, whereas in 64- bit architectures size_t is typically defined as unsigned long. Architecture used during Frama-C translation is controlled through Frama-C -machdep option that specifies the architecture type to use during translation. The default value of -machdep is x86_32 (a 13 CHAPTER 2. WHAT THE PLUG-IN PROVIDES generic 32-bit x86 architecture). Note that since code generated by E-ACSL is aimed at being compiled it is important that the architecture used by Frama-C matches the archi- tecture corresponding to your compiler and your system. For instance, in a 64-bit machine you should also pass -machdep x86_64 option as follows: $ frama-c -machdep x86_64 -e-acsl first.i -then-last \ - print -ocode monitored_first.c This file can be compile with a C compiler (for instance Gcc), as follows: $ gcc -c -Wno-attributes monitored_first.c However, creating an executable through a proper invokation to Gcc is painful and is not documented. Instead, E-ACSL comes with a companion wrapper script for this purpose. 2.2 E-ACSL Wrapper Script Presently, e-acsl-gcc.sh is a recommended way of running the E-ACSL plug-in. This manual further describes features of the E-ACSL plug-in using e-acsl-gcc.sh as its main driver for source code instrumentation and compilation of the instrumented programs. In this section we describe e-acsl-gcc.sh and provide several examples of its use. 2.2.1 Standard Usage The default behaviour of e-acsl-gcc.sh is to instrument an annotated C program with runtime assertions via a run of Frama-C. $ e-acsl-gcc.sh -omonitored_first.i first.i The above command instruments first.i with runtime assertions and outputs the generated code to monitored_first.i. Unless the name of the output file is specified via the -o option (i.e., –omonitored_first.i in the above example), the generated code is placed to a file named a.out.frama.c. Compilation and Linking of the original and the instrumented sources is enabled using the -c option. For instance, command $ e-acsl-gcc.sh -c -omonitored_first.i first.i instruments the code in first.i, outputs it to monitored_first.i and produces 2 executa- bles: a.out and a.out.e-acsl, such that a.out is an executable compiled from first.i, while a.out.e-acsl is an executable compiled from monitored_first.i generated by E- ACSL. You can execute the generate binaries, in particular a.out.e-acsl which detects at runtime the incorrect annotation. $ ./a.out.e-acsl first.i: In function 'main' first.i:4: Error: Assertion failed: The failing predicate is: x == 1. Aborted (core dumped) $ echo $? 134 14 2.2. E-ACSL WRAPPER SCRIPT The execution aborts with a non-zero exit code (134) and an error message indicating an E-ACSL annotation that has been violated. There is no output for the valid E-ACSL annotation. That is, the run of an executable generated from the instrumented source file (i.e., monitored_first.i) detects that the second annotation in the initial program is invalid, whereas the first annotation holds for this execution. Named executables can be created using the -O option. This is such that a value supplied to the -O option is used to name the executable generated from the original program and the executable generated from the E-ACSL-instrumented code is suffixed .e-acsl. For example, command $ e-acsl-gcc.sh -c -omonitored_first.i -Omonitored_first first.i names the executables generated from first.i and monitored_first.i: monitored_first and monitored_first.e-acsl respectively. The e-acsl-gcc.sh -C option allows to skip the instrumentation step and compile a given program as if it was already instrumented by the E-ACSL plug-in. This option is useful if one makes changes to an already instrumented source file by hand and only wants to recompile it. $ e-acsl-gcc.sh -C -Omonitored_first monitored_first.i The above command generates a single executable named monitored_first.e-acsl. This is because monitored_first.i is considered to be instrumented code and thus no original program is provided. 2.2.2 Customising Frama-C and Gcc Invocations By default e-acsl-gcc.sh uses frama-c and gcc executables by looking them up in a sys- tem’s path. If either of the tools are not found the script fails with an appropriate error message. Paths to Frama-C and Gcc executables can also be passed using -I and -G options respectively, for instance as follows: $ e-acsl-gcc.sh -I/usr/local/bin/frama-c -G/usr/bin/gcc6 foo.c Runs of Frama-C and Gcc issued by e-acsl-gcc.sh can further be customized by using additional flags. Frama-C flags can be passed using the -F option, while -e and -l op- tions allow for passing additional pre-processor and linker flags during Gcc invocations. For example, command $ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c yields an instrumented program a.out.frama.c where ACSL formulas are output using the UTF-8 character set. Further, during the compilation of a.out.frama.c Gcc adds directories /bar and /baz to the list of directories to be searched for header files. It is worth mentioning that e-acsl-gcc.sh implements several convenience flags for setting some of the Frama-C options. For instance, -E can be used to pass additional arguments to the Frama-C pre-processor (see Section 2.2.5). 2.2.3 Verbosity Levels and Output Redirection By default e-acsl-gcc.sh prints the executed Frama-C and Gcc commands and pipes their output to the terminal. The verbosity of Frama-C output can be changed using -v 15 CHAPTER 2. WHAT THE PLUG-IN PROVIDES and -d options used to pass values to -verbose and -debug flags of Frama-C respectively. For instance, to increase the verbosity of plug-ins but suppress the verbosity of the Frama-C kernel while instrumenting foo.c one can use the following command: $ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c Verbosity of the e-acsl-gcc.sh output can also be reduced using the -q option that sup- presses any output except errors or warnings issued by Gcc, Frama-C, and e-acsl-gcc.sh itself. The output of e-acsl-gcc.sh can also be redirected to a specified file using the -s option. For example, the following command redirects all output during instrumentation and compilation of foo.c to the file named /tmp/log. $ e-acsl-gcc.sh -c -s/tmp/log foo.c 2.2.4 Architecture Dependency As pointed out in Section 2.1.2 the execution of a C program depends on the underlying machine architecture it is executed on. The program must be compiled on the very same architecture (or cross-compiled for it) for the compiler being able to generate a correct binary. Frama-C makes assumptions about the machine architecture when analyzing source code. By default, it assumes an X86 32-bit platform, but it can be customized through -machdep switch [5]. This option is of primary importance when using the E-ACSL plug-in: it must be set to the value corresponding to the machine architecture which the generated code will be executed on, otherwise the generated program is likely to fail to link against the E-ACSL library. Note that the library is built using the default machine architecture. One of the benefits of using the wrapper script is that it makes sure that Frama-C is invoked with the correct -machdep option. By default e-acsl-gcc.sh uses -machdep gcc_x86_64 for 64-bit architectures and -machdep gcc_x86_32 for 32-bit ones. Compiler invocations are further passed -m64 or -m32 options to generate code using 64-bit or 32-bit ABI respectively. At the present stage of implementation E-ACSL does not support generating executables with ABI different to the default one. 2.2.5 Documentation For full up-to-date documentation of e-acsl-gcc.sh see its man page: $ man e-acsl-gcc.sh Alternatively, you can also use the -h option of e-acsl-gcc.sh: $ e-acsl-gcc.sh -h 2.3 Execution Environment of the Generated Code The environment in which the code is executed is not necessarily the same as the one assumed by Frama-C. You should take care of that when running the E-ACSL plug-in and when compiling the generated code with Gcc. In this aspect, the plug-in offers a few possibilities of customization. 16 2.3. EXECUTION ENVIRONMENT OF THE GENERATED CODE 2.3.1 Runtime Errors in Annotations The major difference between ACSL [2] and E-ACSL [13] specification languages is that the logic is total in the former while it is partial in the latter one: the semantics of a logic construct c denoting a C expression e is undefined if e leads to a runtime error and, consequently, the semantics of any term t (resp. predicate p) containing such a construct c is undefined as soon as e has to be evaluated in order to evaluate t (resp. p). The E-ACSL Reference Manual also states that “it is the responsibility of each tool which interprets E-ACSL to ensure that an undefined term is never evaluated” [13]. Accordingly, the E-ACSL plug-in prevents an undefined term from being evaluated. If an annotation contains such a term, E-ACSL will report a proper error at runtime instead of evaluating it. Consider for instance the following annotated program. File rte.i /∗@ behavior yes: assumes x % y == 0; ensures \result == 1; behavior no: assumes x % y != 0; ensures \result == 0; ∗/ int is_dividable ( int x, int y) { return x % y == 0; } int main(void) { is_dividable (2, 0); return 0; } The terms and predicates containing the modulo ‘%’ in the assumes clause are undefined in the context of the main function call since the second argument is equal to 0. However, we can generate an instrumented code and compile it using the following command: $ e-acsl-gcc.sh -c -omonitored_rte.i -Orte rte.i Now, when rte.e-acsl is executed, you get the following output indicating that your function contract is invalid because it contains a division by zero. $ ./rte.e-acsl RTE failed at line 5 in function is_dividable. The failing predicate is: division_by_zero: y != 0. Aborted 2.3.2 Libc By default, Frama-C uses its own standard library (aka libc) instead of the one of your system. If you do not want to use it, you have to add the option -no-framac-stdlib to the Frama-C command line. It might be particularly useful in one of the following contexts: • several libc functions used by the analyzed program are still not defined in the Frama- C libc; or 17 CHAPTER 2. WHAT THE PLUG-IN PROVIDES • your system libc and the Frama-C libc mismatch about several function types (for instance, your system libc is not 100% POSIX compliant); or • several Frama-C lib functions get a contract and you are not interested in verifying them (for instance, only checking undefine behaviors matters). Notably, e-acsl-gcc.sh disables Frama-C libc by default. This is because most of its functions are annotated with E-ACSL contracts and generating code for these con- tracts results in additional runtime overheads. To enforce default Frama-C contracts with e-acsl-gcc.sh you can pass -L option to the wrapper script. 2.3.3 Integers E-ACSL uses an integer type corresponding to mathematical integers which does not fit in any integral C type. To circumvent this issue, E-ACSL uses the GMP library2 . Thus, even if E-ACSL does its best to use standard integral types instead of GMP [9], it may generate such integers from time to time. It is notably the case if your program contains long long , either signed or unsigned. Consider for instance the following program. File gmp.i unsigned long long my_pow(unsigned int x, unsigned int n) { int res = 1; while (n) { if (n & 1) res *= x; n >>= 1; x *= x; } return res; } int main(void) { unsigned long long x = my_pow(2, 63); /∗@ assert (2 ∗ x + 1) % 2 == 1; ∗/ return 0; } Even on a 64-bit machine, it is not possible to compute the assertion with a standard C type. In this case, the E-ACSL plug-in generates GMP code. Note that E-ACSL library already includes GMP, thus no additional arguments need to be provided. We can generate and execute the instrumented code as usual via the following command: $ e-acsl-gcc.sh -omonitored_gmp.i -Ogmp gmp.i $ ./gmp.e-acsl Since the assertion is valid, there is no output in this case. Note that it is possible to use GMP arithmetic in all cases (even if not required). This option is controlled through -g switch of e-acsl-gcc.sh which passes the -e-acsl-gmp-only option to the E-ACSL plug-in. However it could slow down the execution of the instrumented program significantly. 2 http://gmplib.org 18 2.3. EXECUTION ENVIRONMENT OF THE GENERATED CODE 2.3.4 Memory-related Annotations The E-ACSL plug-in handles memory-related annotations such as \valid . Consider for in- stance the following program. File valid.c #include "stdlib.h" extern void *malloc(size_t); extern void free (void*); int main(void) { int *x; x = (int*)malloc( sizeof ( int )); /∗@ assert \valid(x); ∗/ free (x); /∗@ assert freed: \valid(x); ∗/ return 0; } Even though the first annotation holds, the second annotation (labelled freed) is invalid. This is because at the point of its execution memory allocated via malloc has been deallocated and x is a stale pointer referencing unallocated memory. The execution of the instrumented program thus reports the violation of the second annotation: $ e-acsl-gcc.sh -c -Ovalid valid.c $ ./ valid .e-acsl valid.c: In function 'main' valid.c:11: Error: Assertion failed: The failing predicate is: freed: \valid(x). Aborted (core dumped) To check memory-related predicates (such as \valid ) E-ACSL tracks memory allocated by a program at runtime. E-ACSL records memory blocks in a meta-storage tracking each block’s boundaries (i.e., its base address and length), per-byte initialization and the notion of an address being freeable (i.e., whether it can be safely passed to the free function). During an execution of the instrumented program code injected by E-ACSL transformations queries the meta-storage to identify properties of an address in question. For instance, during the execution of the above program the monitor injected by E-ACSL first records information about the memory block allocated via a call to malloc. Further, during the execution of the first assertion the monitor queries the meta-storage about the address of the memory location pointed to by x. Since the location belongs to an allocated memory block, the meta-storage identifies it as belonging to the tracked allocation. Consequently, the assertion evaluates to true and the monitors allows the execution to continue. The second assertion, however, fails. This is because the block pointed to by x has been removed from the meta-storage by a call to free, and thus a meta-storage query identifies location x as belonging unallocated memory space. E-ACSL Memory Models Memory tracking implemented by the E-ACSL library comes in two flavours dubbed bittree- based and segment-based memory models. With the bittree-based model meta-storage is 19 CHAPTER 2. WHAT THE PLUG-IN PROVIDES implemented as a compact prefix trie called Patricia trie [10], whereas segment-based mem- ory model is based on shadow memory [17]. The functionality of the provided memory models is equivalent, however they differ in performance. We further discuss performance considerations. The E-ACSL models allocate heap memory using a customized version of the dlmalloc3 memory allocator replacing system-wide malloc and similar functions (e.g., calloc or free). At the level of e-acsl-gcc.sh you can choose between different memory models using the -m switch followed by the name of the memory model to link against. For instance, command $ e-acsl-gcc.sh -mbittree -c -Ovalid valid.c links a program generated from valid.c against the library implementing the bittree-based memory model, whereas the following invocation uses shadow-based tracking: $ e-acsl-gcc.sh -msegment -c -Ovalid valid.c It is also possible to generate executables using both models as follows: $ e-acsl-gcc.sh -msegment,bittree -c -Ovalid valid.c In this case, e-acsl-gcc.sh produces 3 executables: valid, valid.e-acsl-segment and valid.e-acsl-bittree corresponding to an executable generated from the original source code, and the executables generated from the E-ACSL-instrumented sources linked against segment-based and bittree-based memory models. Unless specified, E-ACSL defaults to the segment-based memory model. Performance Considerations As pointed out in the previous section the functionalities provided by both segment-based and bittree-based memory models are equivalent but differ in performance. The bittree-based model uses compact memory representation of metadata. The segment-based model on the other hand uses significantly more memory. You can expect over 2x times memory overheads when using it. However It is often an order of magnitude faster than the bittree-based model [17]. Maximized Memory Tracking By default E-ACSL uses static analysis to reduce instrumentation and therefore runtime and memory overheads [12]. With respect to memory tracking this means that E-ACSL may omit recording memory blocks irrelevant for runtime analysis. It is, however, still possible to systematically instrument the code for handling potential memory-related annotations even when it is not required. This feature can be enabled using the -M switch of e-acsl-gcc.sh or -e-acsl-full-mtracking option of the E-ACSL plug-in. The above-mentioned static analysis is probably the less robust part of E-ACSL for the time being. When handling a large piece of code, it might be necessary to deactivate it and systematically instrument the code as explained above. 3 http://dlmalloc.net/ 20 2.3. EXECUTION ENVIRONMENT OF THE GENERATED CODE 2.3.5 Runtime Monitor Behavior When a predicate is checked at runtime, function __e_acsl_assert is called. By default this function does nothing if the predicate is valid, and prints an error message and aborts the execution (by raising an ABORT signal via a call to the C function abort) if the predicate is invalid. If E-ACSL detects that its verdict is not trustable (see Section 2.5.4), it prints a warning with its guess and continues the execution. The default behavior of __e_acsl_assert can be altered using --fail-with-code=CODE option of e-acsl-gcc.sh that uses exit(CODE) instead of abort. For instance, the program generated using the following command exits with code 5 on a predicate violation. $ e-acsl-gcc.sh -c --fail-with-code=5 foo.c Forceful termination of a monitored program can be disabled using --keep-going option. If specified, e-acsl-gcc.sh generates code that reports each property violated at runtime but allows the monitored program to continue execution. --keep-going should be used with caution: such unterminated executions may lead to incorrect verification results. e-acsl-gcc.sh also provides a way to use an alternative definition of __e_acsl_assert. Custom implementation of __e_acsl_assert should be provided in a separate C (or object file) and respect the following signature: void __e_acsl_assert(int predicate, __e_acsl_assert_data_t * data); With data a structure containing the following fields: • blocking: integer representing if the assertion is blocking or not; • kind: C string representing a kind of annotation (e.g., "Assertion"); • pred_txt: stringified predicate; • file: un-instrumented file of predicate placement; • fct: function of predicate placement in the un-instrumented file; • line: line of predicate placement in the un-instrumented file; • values: values contributing to the predicate. Additionally, it may depends on the global variable __e_acsl_sound_verdict. This variable of type int is set to 0 as soon as the verdict provided by E-ACSL is not trustworthy anymore (see Section 2.5.4). Below is an example which prints the validity status of each property but never exits. File my_assert.c #include <stdio.h> #include <e_acsl.h> extern int __e_acsl_sound_verdict; void __e_acsl_assert(int predicate, __e_acsl_assert_data_t * data) { printf ("%s in file %s at line %d in function %s is %s (%s).\n\ 21 CHAPTER 2. WHAT THE PLUG-IN PROVIDES The verified predicate was: `%s'.\n", data->kind, data-> file , data-> line , data->fct, predicate ? "valid" : "invalid", __e_acsl_sound_verdict ? "trustworthy" : "UNTRUSTWORTHY", data->pred_txt); if (data->values) { printf ("With values:\n"); __e_acsl_assert_data_value_t * value = data->values; while (value != NULL) { __e_acsl_print_value(value); value = value->next; } } } A monitored program that uses custom definition of __e_acsl_assert can then be gener- ated as follows using --external-assert option of e-acsl-gcc.sh to replace the default implementation of __e_acsl_assert with the customized one specified in my_assert.c. $ e-acsl-gcc.sh -c -X first.i -Ofirst --external-assert=my_assert.c $ ./ first .e-acsl Assertion in file first.i at line 3 in function main is valid (trustworthy). The verified predicate was: `x == 0'. Assertion in file first.i at line 4 in function main is invalid (trustworthy). The verified predicate was: `x == 1'. The default assertion function prints the values contributing to an assertion along with the error message. $ e-acsl-gcc.sh -c -X first.i -Ofirst $ ./ first .e-acsl first.i: In function 'main' first.i:4: Error: Assertion failed: The failing predicate is: x == 1. With values: - x: 0 This behavior can be overriden by using the --no-assert-print-data option of e-acsl-gcc.sh. $ e-acsl-gcc.sh -c -X first.i -Ofirst --no-assert-print-data $ ./ first .e-acsl first.i: In function 'main' first.i:4: Error: Assertion failed: The failing predicate is: x == 1. As with the assertion function, e-acsl-gcc.sh provides a way to use an alternative definition of __e_acsl_print_value. Custom implementation of __e_acsl_print_value should be provided in a separate C (or object file) and respect the following signature: void __e_acsl_print_value(__e_acsl_assert_data_value_t * value); 22 2.4. ADDITIONAL VERIFICATIONS The details and documentation of the structure __e_acsl_assert_data_value_t can be found in the file e_acsl_assert_data.h distributed with E-ACSL in the installation folder share/frama-c/e-acsl/instrumentation_model. Below is an example which prints only the name of the variable contributing to an assertion. File my_print_value.c #include <stdio.h> #include <e_acsl.h> void __e_acsl_print_value(__e_acsl_assert_data_value_t * value) { printf ("\t- custom print for %s\n", value->name); } A monitored program that uses custom definition of __e_acsl_print_value can then be generated as follows using --external-print-value option of e-acsl-gcc.sh to replace the default implementation of __e_acsl_print_value with the customized one specified in my_print_value.c. $ e-acsl-gcc.sh -c -X first.i -Ofirst \ -- external - print -value=my_print_value.c $ ./ first .e-acsl first.i: In function 'main' first.i:4: Error: Assertion failed: The failing predicate is: x == 1. With values: - custom print for x The custom definitions of __e_acsl_assert and __e_acsl_print_value can be used at the same time. $ e-acsl-gcc.sh -c -X first.i -Ofirst \ -- external -assert=my_assert.c \ -- external - print -value=my_print_value.c $ ./ first .e-acsl Assertion in file first.i at line 3 in function main is valid (trustworthy). The verified predicate was: `x == 0'. With values: - custom print for x Assertion in file first.i at line 4 in function main is invalid (trustworthy). The verified predicate was: `x == 1'. With values: - custom print for x 2.4 Additional Verifications In addition to checking annotations at runtime, E-ACSL is able to detect a few errors at runtime. 2.4.1 Format String Vulnerabilities Whenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format. 23 CHAPTER 2. WHAT THE PLUG-IN PROVIDES File printf.c #include <stdio.h> int main(void) { printf ("is %d really an int?", "foo"); return 0; } This error can be detected by E-ACSL as follows. $ e-acsl-gcc.sh -Oprintf -c --validate-format-strings printf.c $ ./ printf .e-acsl printf : directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'char*' Abort 2.4.2 Incorrect Usage of Libc Functions Whenever option --libc-replacements of e-acsl-gcc.sh is set, E-ACSL is able to detect incorrect usage of the following libc functions: • memcmp • memcpy • memmove • memset • strcat • strncat • strcmp • strcpy • strncpy • strlen For instance, the program below incorrectly uses strcpy because the destination string should contain at least 7 char (and not only 6). File strcpy.c #include <stdlib.h> #include <string.h> int main(void) { char *dst = malloc( sizeof (char) * 6); strcpy(dst, "foobar"); return 0; } This error can be reported by E-ACSL as follows. 24 2.5. INCOMPLETE VERIFICATION $ e-acsl-gcc.sh -Ostrcpy -c --libc-replacements strcpy.c $ ./ strcpy .e-acsl strlen: insufficient space in destination string, at least 7 bytes required Abort 2.5 Incomplete Verification Executing a C program requires to have a complete application. However, the E-ACSL plug-in does not necessarily require to have it to generate the instrumented code. It is still possible to instrument a partial program with no entry point (Section 2.5.1) or in which some functions remain undefined (Section 2.5.2). It is also possible to partially instrument an application in order to reduce the runtime overhead. 2.5.1 Programs with no Main Function The E-ACSL plug-in can instrument a program without the main function. Consider for instance the following annotated program without main. File no_main.i /∗@ behavior even: @ assumes n % 2 == 0; @ ensures \result >= 1; @ behavior odd: @ assumes n % 2 != 0; @ ensures \result >= 1; ∗/ unsigned long long my_pow(unsigned int x, unsigned int n) { unsigned long long res = 1; while (n) { if (n & 1) res *= x; n >>= 1; x *= x; } return res; } The instrumented code is generated as usual, even though you get an additional warning. $ e-acsl-gcc.sh no_main.i -omonitored_no_main.i [kernel] Parsing no_main.i (no preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [e-acsl] Warning: cannot find entry point `main'. Please use option `-main' for specifying a valid entry point. The generated program may miss memory instrumentation if there are memory-related annotations. [e-acsl] translation done in project "e-acsl". This warning indicates that the instrumentation could be incorrect if the program contains memory-related annotations (see Section 3.3.1). That is not the case here, so you can safely ignore it. Now, it is possible to compile the generated code with a C compiler in a standard way, and even link it against additional files such as the following: File main.c 25 CHAPTER 2. WHAT THE PLUG-IN PROVIDES #include "stdio.h" int main(void) { unsigned long long x = my_pow(2, 16); printf ("x = %llu\n",x); return 0; } $ e-acsl-gcc.sh -C monitored_no_main.i main.c -Owith_main $ ./with_main.e-acsl x = 65536 2.5.2 Undefined Functions Similar to the above section E-ACSL is capable of instrumenting a program which has definitions of arbitrary functions missing. Consider for instance the following annotated program for which the implementation of the function my_pow is not provided. File no_code.c #include "stdio.h" /∗@ behavior even: @ assumes n % 2 == 0; @ ensures \result >= 1; @ behavior odd: @ assumes n % 2 != 0; @ ensures \result >= 1; ∗/ extern unsigned long long my_pow(unsigned int x, unsigned int n); int main(void) { unsigned long long x = my_pow(2, 64); return 0; } The instrumented code is generated as usual, even though you get an additional warning. $ e-acsl-gcc.sh -omonitored_no_code.i no_code.c [kernel] Parsing no_code.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] Warning: annotating undefined function `my_pow': the generated program may miss memory instrumentation if there are memory-related annotations. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [e-acsl] translation done in project "e-acsl". Similar to the previous Section the warning indicates that the instrumentation could be incorrect if the program contains memory-related annotations (see Section 3.3.2). That is still not the case here, so you can safely ignore it. File pow.i unsigned long long my_pow(unsigned int x, unsigned int n) { unsigned long long res = 1; while (n) { if (n & 1) res *= x; n >>= 1; 26 2.5. INCOMPLETE VERIFICATION x *= x; } return res; } Similar to the example shown in the previous section you can generate the executable by providing definition of my_pow. $ e-acsl-gcc.sh -C -Ono_code pow.i monitored_no_code.i $ ./no_code.e-acsl no_code.c: In function 'my_pow' no_code.c:5: Error: Postcondition failed: The failing predicate is: even: \result >= 1. Aborted (core dumped) The execution of the corresponding binary fails at runtime: actually, our implementation of the function my_pow overflows in case of large exponentiations. 2.5.3 Providing a White List of Functions By default, the E-ACSL plug-in generates code for checking at runtime all the annotations of the analyzed files. Yet, it is possible to handle only annotations of a given set of functions through the option -e-acsl-functions. This way, no runtime check is generated for anno- tations of all the other functions. It allows the user to focus on a particular part of the code, while reducing the global runtime overhead. 2.5.4 Partial Instrumentation (Experimental) Partial instrumentation is still an experimental feature. It may evolve in the future and/or not work as expected. By default, the E-ACSL plug-in generates all the necessary pieces of code for checking at runtime the provided annotations. This amount of instrumentation may be quite large. It is possible to reduce it by manually specifying the set of functions to be instrumented through the option -e-acsl-instrument. This way, contrary to the option -e-acsl-functions, all the annotations are still checked at runtime. However, since less code is generated, the generated program usually runs faster. However, it may lead to unsound verdicts if it would have been necessary to generate the instrumentation for one of the uninstrumented functions. A typical usage of this option consists in specifying the set of functions to be not instru- mented. For instance, to instrument all functions except functions f and g, you should specify -e-acsl-instrument=+@all,-f,-g. Consider the following example in which all assertions are valid. File partial.i void f( int *p) { *p = 0; } void g(int *p) { *p = 1; 27 CHAPTER 2. WHAT THE PLUG-IN PROVIDES } int main(void) { int t[3]; f(&t[0]); /∗@ assert \initialized (&t[0]); ∗/ t[1] = 1; g(&t[1]); g(&t[2]); /∗@ assert \initialized (&t[1]); ∗/ /∗@ assert \initialized (&t[2]); ∗/ return 0; } One can ask to not instrument function g (i.e. to instrument only functions f and main) through the following command. $ e-acsl-gcc.sh \ -c --oexec-e-acsl partial.out \ --e-acsl-extra="-e-acsl-instrument=+@all,-g" \ partial .i Therefore, running the generated executable partial.out leads to the following verdicts. $ ./ partial .out partial.i: In function 'main' partial.i:16: Warning: no sound verdict for Assertion (guess: ok). the considered predicate is: \ initialized (&t[1]) partial.i: In function 'main' partial.i:17: Warning: no sound verdict for Assertion (guess: FAIL). the considered predicate is: \ initialized (&t[2]) First, there is no message for the first assertion about the initialization of &t[0], meaning that this assertion is silently checked as valid by E-ACSL (see Section 2.3.5). It was made possible because of the complete instrumentation of functions f and main. Second, since function g was not instrumented, no sound verdict may be provided after executing it. It leads to the printed warnings for the last two assertions. The indicated guesses (ok for the first assertion and FAIL for the second one) are the verdicts computed by E-ACSL. They can be trusted if and only if the E-ACSL instrumentation is not necessary for validating the considered annotations. In that particular case, it is not true. For instance, the second guess is incorrect since &t[2] is actually initialized through function g. E-ACSL missed it since this function is not instrumented.. 2.6 Combining E-ACSL with Other Plug-ins As the E-ACSL plug-in generates a new Frama-C project, it is easy to run any plug-in on the generated program, either in the same Frama-C session (thanks to the option -then or through the GUI), or in another one. The only issue might be that, depending on the plug-in, the analysis may be imperfect if the generated program uses GMP or the dedicated memory library: both make intensive use of dynamic structures which are usually difficult to handle by analysis tools. 28 2.7. CUSTOMIZATION Another way to combine E-ACSL with other plug-ins is to run E-ACSL last. For instance, the RTE plug-in [7] may be used to generate annotations corresponding to runtime errors. Then the E-ACSL plug-in may generate an instrumented program to verify that there are no such runtime errors during the execution of the program. Consider the following program. File combine.i int main(void) { int x = 0 xffff ; int y = 0xfff; int z = x + y; return 0; } To check at runtime that this program does not perform any runtime error (which are po- tential overflows in this case), just do: $ frama-c -rte combine.i -then -e-acsl -then-last -print -ocode monitored_combine.c $ e-acsl-gcc.sh -C -Ocombine monitored_combine.c $ ./combine.e-acsl Automatic assertion generation can also be enabled via e-acsl-gcc.sh directly via the fol- lowing command: $ e-acsl-gcc.sh -c -Ocombine -omonitored_combine.i --rte=all combine.i Note the use of e-acsl-gcc.sh --rte option which asks Frama-C to combine E-ACSL with RTE plug-in. This plug-in automatically instruments the input program with runtime assertions before running the E-ACSL plug-in on it. --rte option of e-acsl-gcc.sh also accepts a comma-separated list of arguments indicating the types of assertions to generate. Consult the e-acsl-gcc.sh man page for a detailed list of arguments accepted by --rte. The present implementation of e-acsl-gcc.sh does not fully support combining E-ACSL with other Frama-C plug-ins. However it is still possible to instrument programs with E-ACSL directly and use e-acsl-gcc.sh to compile the generated code. In this context, the E-ACSL plug-in does not generate code for annotations proven valid by another plug-in, except if you explicitly set the option -e-acsl-valid. For instance, Eva [3] is able to prove that there is no potential overflow in the previous program, so the E-ACSL plug-in does not generate additional code for checking them if you run the following command. $ frama-c -rte combine.i -then -eva -then -e-acsl \ -then-last -print -ocode monitored_combine.i The additional code will be generated with the two following command. $ frama-c -rte combine.i -then -eva -then -e-acsl \ -e-acsl-valid -then-last -print -ocode monitored_combine.i 2.7 Customization There are several ways to customize the E-ACSL plug-in. 29 CHAPTER 2. WHAT THE PLUG-IN PROVIDES First, the name of the generated project – which is e-acsl by default – may be changed by setting the option -e-acsl-project option of the E-ACSL plug-in. While there is not direct support for this option in e-acsl-gcc.sh you can pass it using -F switch: File check.i int main(void) { int x = 0; /∗@ assert x == 0; ∗/ /∗@ assert x << 2 == 0; ∗/ return 0; } $ e-acsl-gcc.sh -F"-e-acsl-project foobar" check.i [kernel] Parsing check.i (no preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [e-acsl] translation done in project "foobar". 2.8 Verbosity Policy By default, E-ACSL does not provide much information when it is running. Mainly, it prints a message when it begins the translation, and another one when the translation is done. It may also display warnings when something requires the attention of the user, for instance if it is not able to translate an annotation. Such information is usually enough but, in some cases, you might want to get additional control on what is displayed. As quite usual with Frama-C plug-ins, E-ACSL offers two different ways to do this: the verbosity level which indicates the amount of information to display, and the message categories which indicate the kind of information to display. 2.8.1 Verbosity Level The amount of information displayed by the E-ACSL plug-in is settable by the option -e-acsl-verbose. It is 1 by default. Below is indicated which information is displayed according to the verbosing level. The level n also displays the information of all the lower levels. -e-acsl-verbose 0 only warnings and errors -e-acsl-verbose 1 beginning and ending of the translation -e-acsl-verbose 2 different parts of the translation and functions-related information -e-acsl-verbose 3 predicates- and statements-related information -e-acsl-verbose 4 terms- and expressions-related information 2.8.2 Message Categories The kind of information to display is settable by the option -e-acsl-msg-key (and unsettable by the option -e-acsl-msg-key-unset). The different keys refer to different parts of the translation, as detailed below. 30 2.8. VERBOSITY POLICY analysis minimization of the instrumentation for memory-related annotation (section 2.3.4) preparation duplication of functions with contracts (section 2.5.2) translation translation of an annotation into C code typing minimization of the instrumentation for integers (section 2.3.3) 31 Chapter 3 Known Limitations The development of the E-ACSL plug-in is still ongoing. First, the E-ACSL reference manual [13] is not yet fully supported. Which annotations can already be translated into C code and which cannot is defined in a separate document [14]. Second, even though we do our best to avoid them, bugs may exist. If you find a new one, please report it on the bug tracking system1 (see Chapter 10 of the Frama-C User Manual [5]). Third, there are some additional known limitations, which could be annoying for the user in some cases, but are tedious to lift. Please contact us if you are interested in lifting these limitations2 . 3.1 Supported Systems The only well-supported system is a Linux distribution on a 64-bit architecture. 3.1.1 Operating Systems Non-Linux systems are almost not yet experimented. It might work but there are most probably issues, in particular if using a non-standard libc. For instance, there are known bugs under Mac OS X3 . 3.1.2 Architectures and Runtime Library The segment-based memory model (used by default for monitoring memory properties such as \valid ) assumes little-endian architecture and has very limited support for 32-bit archi- tectures. When using a 32-bit machine or big-endians, we recomend using the bittree-based memory model instead. The runtime library is also not thread-safe. 3.2 Uninitialized Values As explained in Section 2.3.1, the E-ACSL plug-in should never translate an annotation into C code which can lead to a runtime error. This is enforced, except for uninitialized values 1 https://git.frama-c.com/pub/frama-c/-/issues 2 Read https://git.frama-c.com/pub/frama-c/blob/master/CONTRIBUTING.md for additional details. 3 See for instance at https://bts.frama-c.com/view.php?id=2369 33 CHAPTER 3. KNOWN LIMITATIONS which are values read before having been written. File uninitialized.i int main(void) { int x; /∗@ assert x == 0; ∗/ return 0; } If you generate the instrumented code, compile it, and finally execute it, you may get no runtime error depending on your C compiler, but the behavior is actually undefined because the assertion reads the uninitialized variable x. You should be caught by the E-ACSL plug-in, but that is not the case yet. $ e-acsl-gcc.sh uninitialized.i -c -Omonitored_uninitialized monitored_uninitialized.i: In function 'main': monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this function [-Wuninitialized] $ ./ monitored_uninitialized .e-acsl This is more a design choice than a limitation: should the E-ACSL plug-in generate addi- tional instrumentation to prevent such values from being evaluated, the generated code would be much more verbose and slower. If you really want to track such uninitializations in your annotation, you have to manually add calls to the E-ACSL predicate \initialized [13]. 3.3 Incomplete Programs Section 2.5 explains how the E-ACSL plug-in is able to handle incomplete programs, which are either programs without main, or programs containing undefined functions (i.e. functions without body). However, if such programs contain memory-related annotations, the generated code may be incorrect. That is made explicit by a warning displayed when the E-ACSL plug-in is running (see examples of Sections 2.5.1 and 2.5.2). 3.3.1 Programs without Main The instrumentation in the generated program is partial for every program without main containing memory-related annotations, except if the option -e-acsl-full-mtracking or the E-ACSL plug-in (of -M option of e-acsl-gcc.sh) is provided. In that case, violations of such annotations are undetected. Consider the following example. File valid_no_main.c #include "stdlib.h" extern void *malloc(size_t); extern void free (void*); int f(void) { int *x; 34 3.3. INCOMPLETE PROGRAMS x = (int*)malloc( sizeof ( int )); /∗@ assert \valid(x); ∗/ free (x); /∗@ assert freed: \valid(x); ∗/ return 0; } You can generate the instrumented program as follows. $ e-acsl-gcc.sh -M -omonitored_valid_no_main.i valid_no_main.c [kernel] Parsing valid_no_main.c (with preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Warning: no entry point specified: you must call functions `__e_acsl_globals_init', `__e_acsl_globals_clean', `__e_acsl_memory_init' and `__e_acsl_memory_clean' by yourself. [e-acsl] translation done in project "e-acsl". The last warning states an important point: if this program is linked against another file containing main function, then this main function must be modified to insert a calls to the functions __e_acsl_globals_init and __e_acsl_memory_init at the very beginning. These functions play a very important role: the latter initializes metadata storage used for tracking of memory blocks while the former initializes tracking of global variables and constants. Unless these calls are inserted the run of a modified program is likely to fail. While it is possible to add such intrumentation manually we recommend using e-acsl-gcc.sh. Consider the following incomplete program containing main: File modified_main.c int main(int argc, char **argv) { f(); return 0; } Then just compile and run it as explained in Section 2.3.4. $ e-acsl-gcc.sh -M -omonitored_modified_main.i modified_main.c $ e-acsl-gcc.sh -C -Ovalid_no_main monitored_modified_main.i monitored_valid_no_main.i $ ./valid_no_main.e-acsl Assertion failed at line 11 in function f. The failing predicate is: freed: \valid(x). Aborted Also, if the unprovided main initializes some variables, running the instrumented code (linked against this main) could print some warnings from the E-ACSL memory library4 . 3.3.2 Undefined Functions The instrumentation in the generated program is partial for a program p if p contains a memory-related annotation a and an undefined function f such that: • either f has an (even indirect) effect on a left-value occurring in a; • or a is one of the post-conditions of f . A violation of such an annotation a is undetected. There is no workaround yet. 4 see https://bts.frama-c.com/view.php?id=1696 for an example 35 CHAPTER 3. KNOWN LIMITATIONS 3.3.3 Incomplete Types The instrumentation in the generated program is partial for a program p if p contains a memory-related annotation a and a variable v with an incomplete type definition such that a depends on v (even indirectly). A violation of such an annotation a is undetected. There is no workaround yet. 3.4 Recursive Functions Programs containing recursive functions have the same limitations as the ones containing undefined functions (Section 3.3.2) and memory-related annotations. 3.5 Variadic Functions Programs containing undefined variadic functions with contracts are not yet supported. Using the Variadic plug-in of Frama-C could be a solution in some cases, but its generated code cannot always be compiled. 3.6 Function Pointers Programs containing function pointers have the same limitations on memory-related annota- tions as the ones containing undefined or recursive functions. 3.7 Requirements to Input Programs 3.7.1 E-ACSL Namespace While E-ACSL uses source-to-source transformations and not binary instrumentations it is important that the source code provided as input does not contain any variables or functions prefixed __e_acsl_. E-ACSL reserves this namespace for its transformations, and there- fore an input program containing such symbols beforehand may fail to be instrumented or compiled. 3.7.2 Memory Management Functions Programs providing custom definitions of syscall, mmap or sbrk should be rejected. Also, an input programs should not modify memory-management functions namely malloc, calloc, realloc, free, cfree, posix_memalign and aligned_alloc. E-ACSL relies on these func- tions in order to track heap memory. Further, correct heap memory monitoring requires to limit allocation and deallocation of heap memory to POSIX-compliant memory management functions listed above. Monitoring of programs that allocate memory using non-standard or obsolete functions (e.g., valloc, memalign, pvalloc) may not work correctly. 36 Appendix A Changes This chapter summarizes the changes in this documentation between each E-ACSL release. First we list changes of the last release. E-ACSL 24.0 Chromium • Runtime Monitor Behavior: Document new options --assert-print-data and --external-print-value of e-acsl-gcc.sh, and update documentation for option --external-assert. E-ACSL 22.0 Titanium • Update every section with changes to Frama-C and e-acsl-gcc.sh output • Simple Example: Remove option -e-acsl-check • Combining E-ACSL with Other PLug-ins: -e-acsl-prepare is no more neces- sary. E-ACSL 19.0 Potassium • Runtime Monitor Behavior: Document global variable __e_acsl_sound_verdict usable in __e_acsl_assert. • New section Partial Instrumentation. • New section Providing a White List of Functions. E-ACSL 18.0 Argon • Introduction: Improve a bit and reference new related papers. • What the Plug-in Provides: Highlight that the memory analysis is not yet robust. • What the Plug-in Provides: Highlight the importance of -e-acsl-prepare. 37 APPENDIX A. CHANGES • Known Limitations: Replace section “Limitations of E-ACSL Monitoring Libraries” by the new section “Supported Systems”. • Known Limitations: Add limitation about monitoring of variables with incomplete types. E-ACSL Chlorine-20180501 • New section Additional Verifications. • Update every section with respect to the changes introduced since E-ACSL Sulfur- 20180101. E-ACSL Sulfur-20180101 • no changes E-ACSL Phosphorus-20170501 • Removed chapter Easy Instrumentation with E-ACSL. • What the Plug-in Provides: added section E-ACSL Wrapper Script. • What the Plug-in Provides: added description of E-ACSL runtime libraries. • Known Limitations: added section Requirements to Input Programs. • Known Limitations: added section Limitations of E-ACSL Monitoring Li- braries. • Recursive Functions: remove limitation about possible uses before being declared. • Variadic Functions: mention the Variadic plug-in. E-ACSL 0.6 • Easy Instrumentation with E-ACSL: new chapter. E-ACSL 0.5 • Libc: new section. • Architecture Dependent Annotations: add a remark about Gcc’s machdep. • Use -then-last whenever possible. • Update output wrt Frama-C Sodium changes. • Bibliography: fix incorrect links. 38 E-ACSL 0.4 • No change. E-ACSL 0.3 • Introduction: reference the E-ACSL tutorial. • Memory-related Annotations: document the E_ACSL_MACHDEP macro. E-ACSL 0.2 • First release of this manual. 39 BIBLIOGRAPHY Bibliography [1] Patrick Baudin, François Bobot, Loïc Correnson, and Zaynah Dargaye. Frama-C’s WP plug-in. http://frama-c.com/download/frama-c-wp-manual.pdf. [2] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language. [3] David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin Perelle, and Virgile Prevosto. EVA – The Evolved Value Analysis plug-in. https://frama-c.com/download/frama-c-value-analysis.pdf. [4] Lori A. Clarke and David S. Rosenblum. A historical perspective on runtime asser- tion checking in software development. ACM SIGSOFT Software Engineering Notes, 31(3):25–37, 2006. [5] Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski. Frama-C User Manual. https://frama-c.com/download/frama-c-user-manual.pdf. [6] Mickaël Delahaye, Nikolai Kosmatov, and Julien Signoles. Common specification lan- guage for static and dynamic analysis of C programs. In the 28th Annual ACM Sympo- sium on Applied Computing (SAC), pages 1230–1235. ACM, March 2013. [7] Philippe Herrmann and Julien Signoles. Annotation Generation: Frama-C’s RTE plug- in. http://frama-c.com/download/frama-c-rte-manual.pdf. [8] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A Software Analysis Perspective. Formal Aspects of Comput- ing, pages 1–37, jan 2015. [9] Nikolai Kosmatov, Fonenantsoa Maurica, and Julien Signoles. Efficient Runtime Asser- tion Checking for Properties over Mathematical Numbers. In International Conference on Runtime Verification (RV), October 2020. [10] Nikolaï Kosmatov, Guillaume Petiot, and Julien Signoles. An optimized memory moni- toring for runtime assertion checking of C programs. In International Conference on Run- time Verification (RV 2013), volume 8174 of LNCS, pages 167–182. Springer, September 2013. [11] Nikolaï Kosmatov and Julien Signoles. A lesson on runtime assertion checking with Frama-C. In International Conference on Runtime Verification (RV 2013), volume 8174 of LNCS, pages 386–399. Springer, September 2013. 41 BIBLIOGRAPHY [12] Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles. Soundness of a dataflow analysis for memory monitoring. In Workshop on Languages and Tools for En- suring Cyber-Resilience in Critical Software-Intensive Systems (HILT), November 2018. [13] Julien Signoles. E-ACSL: Executable ANSI/ISO C Specification Language. http://frama-c.com/download/e-acsl/e-acsl.pdf. [14] Julien Signoles. E-ACSL. Implementation in Frama-C Plug-in E-ACSL. http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf. [15] Julien Signoles. From Static Analysis to Runtime Verification with Frama-C and E- ACSL, July 2018. Habilitation Thesis. [16] Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov. E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs. Tool Paper. In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES), September 2017. [17] Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov. Shadow state encoding for efficient monitoring of block-level properties. In International Symposium on Memory Management (ISMM), pages 47–58. ACM, June 2017. 42 INDEX Index –omonitored_first.i, 14 -framac-stdlib, 17 Function ACSL, 9, 13, 17 Input, 36 --assert-print-data, 37 Not Instrumented, 27 Pointer, 36 -C, 15 Recursive, 36 -c, 14 Undefined, 26, 35 Variadic, 36 -d, 16 White List, 27 -debug, 16 dlmalloc, 20 -G, 15 -g, 18 -E, 15 Gcc, 14 -e, 15 GMP, 18, 28 -e-acsl, 11, 12 -e-acsl-full-mtracking, 20, 34 -h, 16 -e-acsl-functions, 27 -e-acsl-gmp-only, 18 -I, 15 -e-acsl-instrument, 27 Installation, 9 -e-acsl-msg-key, 30 integer, 18 -e-acsl-msg-key-unset, 30 -e-acsl-project, 30 --keep-going, 21 -e-acsl-valid, 29 -L, 18 -e-acsl-verbose, 30 -l, 15 -e-acsl-verbose 0, 30 Libc, 17, 24, 33 -e-acsl-verbose 1, 30 --libc-replacements, 24 -e-acsl-verbose 2, 30 -e-acsl-verbose 3, 30 -M, 20, 34 -e-acsl-verbose 4, 30 -m, 20 -e-acsl-version, 9 -m32, 16 e_acsl_assert, 13, 21–23 -m64, 16 __e_acsl_globals_init, 35 Mac OS X, 33 __e_acsl_memory_init, 35 -machdep, 13, 14, 16 e_acsl_print_value, 22, 23 -machdep gcc_x86_32, 16 e_acsl_sound_verdict, 21 -machdep gcc_x86_64, 16 Eva, 9, 29 --external-assert, 22, 37 --no-assert-print-data, 22 --external-print-value, 23, 37 -no-framac-stdlib, 17 -F, 15, 30 -O, 15 --fail-with-code=CODE, 21 -o, 14 Format String Vulnerabilities, 23 -ocode, 13 43 INDEX -print, 12 Program Without main, 25, 34 -q, 16 RTE, 9, 29 --rte, 29 Runtime Error, 17 -s, 16 -then, 28 -then-last, 12 Type Incomplete, 36 Uninitialized value, 33 -v, 15 --validate-format-strings, 23 Variadic, 36, 38 -verbose, 16 WP, 9 Wp, 9 44