WP 0.4 (Draft Manual) - Frama-C
Contents
1. wp warning Missing RTE guards wp Alt Ergo Goal store_swap_post_2_B Valid wp Alt Ergo Goal store_swap_post_1_A Valid As expected Alt Ergo discharged the two proof obligations generated by WP for the swap contract You should notice the warning Missing RT E guards emitted by the WP plug in That is the weakest precondition calculus implemented in WP relies on the hypothesis that your program is runtime error free In this example the swap function dereferences its two parameters and these two pointers should be valid The WP plug in does not generate proof obligation to prevent your program from raising a runtime error because this property may be validated with any other technique for instance by running the value analysis plug in or the rte generation one Hence consider the following new contract for swap File swap2 c requires valid a amp amp valid b ensures A a old b ensures B b old a O assigns a b x void swap int a int b For simplicity the WP plug in is able to run the rte generation plug in for you Now WP reports that the function swap fulfills its contract 1 3 WEAKEST PRECONDITIONS frama c wp wp rte swap c swap2 c kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swap2 c rte annotating function swap wp WP simplified Goal store_swap_function_assigns Valid wp Alt Ergo Goal store_s2. 5 is dedicated to those pointers that are formal parameters of function passed by reference 3 1 Language of Proof Obligations The work of WP consists in translating C and ACSL constructs into first order logical formule We denote by the logic language for constructing proof obligations Shortly this logical language is made of terms t term and propositions P prop made of e Natural signed unbounded integer constants and their operations e Natural real numbers and their operations e Arrays as total maps and tuples 23 CHAPTER 3 WP MODELS Abstract polymorphic data types e Anonymous function symbols Logical connectors e Universally and existentially quantified variables Actually the task of the memory model consists in mapping any heap C values at a given program point to some variable or term in the logical language 3 2 The Hoare Memory Model This is the simplest model inspired by the historical definition of Weakest Precondition Cal culus for programs with no pointers In such programs each global and local variable is assigned a distinct variable in Consider for instance the statement x where x has been declared as an int In the Hoare memory model this C variable will be assigned to two variables say 11 before the statement and x after the statement with the obvious relation x2 x 1 if no overflow occurred Of course this model is not capable of handli
3. b Enable slicing 5 b tmp a x 6 return void swap int a int Dependencies gt 17 WP int tmp y Model Store i bli Prover Alt Ergo Y pr O RTE C Split Invariants C Trace Occurrence Figure 2 1 WP in the Frama C GUI File Project Analyses Help Scripts Timeout 10 2 Process 4 B Slicing Information Messages Console Properties WP Proof Obligations T peia Function swa Metrics iia Figure 2 2 WP run from the GUI 14 aa 20 Source file O requires valid a a valid b swap c AAA o ensures A old a old b 1 void swap int a int b h swap o ensures B old b old a 3 int tm a nn o assigns a b 4 a b swap2 c T 5 b tmp void swap int a int b N dia WP int tmp Y tmp a Model Store A Mi x b tmp Prover Alt Ergo v remira O RTE Split Invariants Trace 3 Scripts Timeout 10 C Process 4 Slicing Information Messages Console Properties WP Proof Obligations Impact Module Function Behavior Model Property Kind WP Alt Ergo Coq Z3 Simplify Vampire Cvc3 Metrics swap c swap store post_1_A Property Occurrence ae gt 1Goal store swap post 1 A gt Obligation 2 forall b 0 pointer _ 3 forall a 0 pointer Description 4 forall m 0 data farray Environment 5 forall ta 0 int farray 6 global ta 0
4. gt Alt Ergo 7 valid ta_ 0 a0 1 gt 8 valid ta 0 b 0 1 gt 9 let tmp 0 sint32 of data m 0 a 0 in 10 let m 1 m 0 a 0 gt m 0 b 0 in 11 let m 2 m 1 b 0 gt data of sint32 tmp 0 in v 2 2 COMMAND LINE OPTIONS Source Panel On the center of the Frama C window the status of each code annotation is reported in the left margin The meaning of icons is the same for all plug ins in Frama C and more precisely described in the general user s manual of the platform The status emitted by the WP plug in are Icons for properties No proof attempted The property has not been validated The property is valid but has dependencies 800 The property and all its dependencies are valid Proof Obligations Panel This panel is dedicated to the WP plug in It shows the gener ated proof obligations and their status for each prover By clicking on a prover column you can also submit a proof obligation to a prover by hand By double clicking an annotation you can view its mathematical definition in a human readable format Properties Panel This panel summarizes the consolidated status of properties from vari ous plug ins This panel is not automatically refreshed You should press the Refresh button to update it This panel is described in more details in the general Frama C platform user s manual Property Dependency Graph By double clicking on the status column of a property in the properties panel you can di
5. none of the pointer values contained in variables a and b is stored in memory The only occurrences of these pointer values are in expressions a and b Thus there can be no alias with these pointer values elsewhere in memory provided they are not aliased initially Hence not only can a and b be managed by the Hoare model but we can also treat a and b expressions as two independent variables of type int with the Hoare memory model For the callers of the swap function we can also take benefit from such by reference passing arguments Typically consider the following caller program void f void int x lye swap amp x amp y Strictly speaking this program takes the addresses of x and y Thus it would be natural to handle those variables by a model with pointers However swap will actually always use amp x and amp y which are respectively x and y In such a situation it is then correct to handle those variables with the Hoare model and this is a very effective optimization in practice Notice however that in the example above the optimization is only correct because x and y have disjoint addresses These optimizations can be activated in the WP plug in with the wp byreference op tion and the necessary separation conditions are generated on the fly To summarize the wp byreference option e detects pointer or array variables that are always passed by reference e generates additional pre conditions to preve
6. valid before stmt such that Q holds after the execution of stmt Hoare s triples In mathematical terms we denote such a property by a Hoare s triple P stmt Q which reads whenever P holds then after running stmt Q holds CHAPTER 1 INTRODUCTION Thus we can define the weakest precondition as a function wp over statements and properties such that the following Hoare triple always holds wp stmt Q stmt Q For instance consider a simple assignment over an integer local variable x we have r 1 gt 0 x x 1 x gt 0 It should be intuitive that in this simple case the weakest precondition for this assignment of a property Q over x can be obtained by replacing x with x 1 in Q More generally for any statement and any property it is possible to define such a weakest precondition Verification Consider now function contracts We basically have pre conditions assertions and post conditions Say function f has a precondition P and a post condition Q we now want to prove that f satisfies its contract which can be formalized by P f Q Consider now W wp f Q we have by definition of wp W f Q Suppose now that we can prove that P entails W we can use the intermediate result of the weakest precondition calculus to prove the function contracts This operation can be summarized by the following diagram Bm Wi P Q This is the main idea of how to prove a property by weakest precondit
7. ES MIXED WITH POINTERS Typically consider the statement p where p is a C variable of type int The memory model M will assign a unique pointer value P 7 to the address of p in memory Then it retrieves the actual value of the pointer p say Ap by reading a value of type int into the memory variables m at address P Ap readintx mM P Next the model retrieves the previous int value at actual address Ap say Vp Vp readint Ap Finally the model relates the final memory state m with the incremented value V 1 at address P writeint M Ap Vp 1 m There are two such models with pointers available with the WP plug in wp model Store asimple memory model with two heap variables One is for the allocation table that deals with pointer validity The second one stores numerical and pointer values into an array indexed by pointers This model is not capable of handling unions and casts of pointer types wp model Runtime a low level memory model also with two heap variables One is for the allocation table and second one stores all values of the heap as an array of bytes indexed by pointers All operations can be handled by this model but the generated proof obligations are generally untractable by automated decision procedures 3 4 Hoare Variables mixed with Pointers As illustrated above a very simple statement is generally translated by memory models into complex formulse However it is possibl
8. Software Analyzers WP 0 4 Draft Manual cen List WP Plug in Draft Manual Version 0 4 for Nitrogen 20111001 Loic Correnson Zaynah Dargaye Anne Pacalet CEA LIST Software Safety Laboratory 2010 2011 CEA LIST This work has been supported by the U3CAT ANR project Contents 1 Introduction 7 1 1 Installation 2 2 ccoo Oe ee a a aa 8 1 2 Tutorial ss 2 sank a8 sa ae 4 eae eee re e da 8 1 3 Weakest Preconditions lt gt o s esci ee au san ss an nun 9 1 4 Memory Models gt se c seriu bbe 4 2 0 4 a Ha as Es ana 11 2 Using WP Plug in 13 2 1 Graphical User Interfaee cocos 2a sau a a Se an da 13 22 Command Line Opli scores ae ae ER EA eS 15 22 1 Aal OER a oe ek ole ate ler Me ke BM a ee A ae ech 16 2 22 Program Entry Point 4 4 66 ea haps oh a wh we aed 16 2 2 3 Model Selecta 2c us anne an e eae ae he RA 17 224 Computation Strategy s 4 4 64 u kw a nr we ES 17 2 2 5 Decision Procedures Interface o 18 2 2 6 Generated Proof Obligations o onen 19 2 3 Plug in Developer Interface 200020002 ee eee 21 2 4 Plug in Persistent Data e e 21 3 WP Models 23 3 1 Language of Proof Obligations CC no onen 23 3 2 The Hoare Memory Model s c sics s a os a au nen a en ae a h 24 3 3 Memory Models with Pointers 2 2 2 22 Eon onen 24 3 4 Hoare Variables mixed with Pointers 2 2 o nenn 25 3 5 Hoare Variables
9. e in some situations to mix the Hoare memory model with the other ones For instance assume the address of variable x is never taken in the program Hence it is not possible to create a pointer aliased with amp x It is thus legal to manage the value of x with the Hoare memory model and other values with another memory model M that deals with pointers Common occurrences of such a situation are pointer variables For instance assume p is a variable of type int it is often the case that the value of p is used as in p but not the address of the variable p itself namely amp p Then it is very efficient to manage the value of p with the Hoare memory model and the value of p with a memory model with pointers Such an optimization is possible whenever the address of a variable is never taken in the program It is activated by default in the WP plug in since it is very effective in practice You can nevertheless deactivate it with option wp no logicvar 25 CHAPTER 3 WP MODELS 3 5 Hoare Variables for Reference Parameters A common programming pattern in C programs is to use pointers for function arguments passed by reference For instance consider the swap function below void swap int a int b int tmp a xa b b tmp Since neither the address of a nor the one of b are taken their values can be managed by the Hoare Model as described in previous section But we can do even better Remark that
10. ed to The format of this file is private to the WP plug in It is however a regular text file from which you can cut and paste part of previously written script proofs The WP plug in manages the content of this file for you wp proof coq only runs cogc on proof scripts found in the script file If the generated goal or the default one is not correctly typed checked by coqc the coq prover fails to discharge the proof obligation wp proof coqide first tries to replay some known proof script if any If it does not succeed then a new interactive session for coqide is opened During this session several files are opened for you lt goal gt v the proof obligation to discharge lt model gt _env lt n gt v the environment generated during weakest precondition calculus already compiled by coqc type definitions global variables etc lt model gt _model v the definitions and properties of the memory model used already compiled by coqc f script the script file where all your proofs are stored This is useful for reusing parts from previous scripts on similar goals As soon as cogide exits the edited proof script is saved back to the script file and finally checked by coqc Do not forget to save your proof before exiting coqide Why Finally a wide range of automated provers are supported by WP thanks to the Why 2 29 prover interface Both the why translation tool and the why dp utility are required You also need to install ext
11. entions Their Coq instances are copied on the temporary directory for separate compilation purposes To discharge a proof obligation WP assembles an input for the external decision prover composed of three inputs the resources for selected memory model the resources from the environment of the goal and the goal itself Remark to save space on disk when generating proof obligations from the command line the proof obligations are only generated for the requested prover format This behavior is turned off under the Gui and in debug mode Hence you still get all formats available for all provers in these cases 2 3 Plug in Developer Interface The WP plug in has several entry points registered in the Dynamic module of Frama C Wp run runs the weakest precondition calculus using the options to know what to compute This is similar to using wp on the command line Wp wp_compute kf_opt bhv_list_opt prop_opt where e kf_ opt is an optional kernel function e bhv_list_opt specifies an optional behavior list e prop_opt specifies an optional property These entry points actually run the WP plug in in the same way than the command line options do 2 4 Plug in Persistent Data As a general observation almost none of the internal WP data is kept in memory after each execution Most of the generated proof obligation data is stored on disk before being sent to provers and they are stored in a temporary directory that is removed up
12. eplaced by function call or predicates by closure conversion wp rte generates RTE guards before computing weakest preconditions This option calls the rte generation plug in with the following options rte mem rte div rte signed and rte unsigned ov The generated guards when proved fulfill the requirements for using the WP plug in wp no simpl deactivates simplification of constant expressions and tautologies wp split conjunctions in generated proof obligations are recursively split into sub goals The generated goal names are suffixed by partn Notice that this option is set by default for assigns clauses when using the effect assigns method see wp assigns above wp split dim lt d gt limits the number of generated sub goals for assigns goals when using wp split The number of generated sub goals will not exceed 2 proof obligations Default is 2 2 2 5 Decision Procedures Interface When the wp proof option is selected proof obligations are sent to a decision procedure If proof obligations have just been generated by using wp wp fct wp bhv or wp prop then only the new proof obligations are sent Otherwise all unproved proof obligations are sent wp check lt dp gt only checks the syntax of generated proof obligations for a family of decision procedures Possible values of dp are alt ergo coq and why wp par lt n gt limits the number of parallel process runs for decision procedures Defau
13. ernal provers by your own Currently the provers you can use with WP and Why and the corresponding values for the wp proof option are simplify yices cvc3 vampire z3 zenon 2 2 6 Generated Proof Obligations Your proof obligations are generated and saved to several text files With the wp out option you can specify a directory of your own where all these files are generated By default this output directory is determined as follows under the GUI it is lt home gt frama c wp where lt home gt is the user s home directory returned by the HOME environment variable In command line a temporary directory is automatically created and removed at Frama C exit The other options controlling the output of generated proof obligations are wp print pretty prints the generated proof obligations on the standard output Results obtained by provers are reported as well wp warnings displays details when warnings are emitted during proof obligation generation wp out lt dir gt sets the user directory where proof obligations are saved The directory is created if it does not exist yet Its content is not cleaned up automatically 19 CHAPTER 2 USING WP PLUG IN wp dot generates a graphical representation of the CFG in the dot format used by the GraphViz tools The output directory contains a lot of files All files are generated with the following naming convention lt goal gt _head txt asummary of the generated proo
14. f obligation This file contains the warning emitted during weakest precondition calculus lt goal gt _body txt a human readable description of the proof obligation lt goal gt _log_ lt prover gt txt a log from the prover when it has been run on the goal The complete goal submitted to external provers lt goal gt _po why for WHY lt goal gt _po_why lt ext gt generated by WHY for external decision procedures lt goal gt _po_ergo why for Alt Ergo without arrays lt goal gt _po_aergo why for Alt Ergo with arrays lt goal gt _po v for Coq Each complete goal actually consists of the specification of the model an environment de scribing the C definitions of your program and the elementary goal itself The environments are lt env gt txt in human readable description of the environment lt env gt why for Why lt env gt _ergo why for Alt Ergo without arrays lt env gt _aergo why for Alt Ergo with arrays lt env gt v for Coq The elementary goals are lt goal gt why the elementary goal generated for WHY lt goal gt _ergo why the elementary goal generated for Alt Ergo without arrays lt goal gt _aergo why the elementary goal generated for Alt Ergo with arrays lt goal gt v the elementary goal generated for Coq http www graphviz org 20 2 3 PLUG IN DEVELOPER INTERFACE Finally definitions and properties of the memory model are distributed in the Frama C share wp directory with similar naming conv
15. for Reference Parameters 000 26 Chapter 1 Introduction This document describes a Frama C plug in that uses external decision procedures to prove ACSL annotations of C functions The WP plug in is named after Weakest Precondition calculus a technique used to prove pro gram properties initiated by Hoare Hoa69 Floyd F1067 and Dijkstra Dij68 Recent tools implement this technique with great performances for instance Boogie Lei08 and Why Fil03 There is already a Frama C plug in Jessie MM09 developed at INRIA that implements a weakest precondition calculus for C programs by compiling them into the Why language The WP plug in is a novel implementation of such a Weakest Precondition calculus for an notated C programs which focuses on parametrization w r t the memory model It is a complementary work to Jessie plug in which relies on a separation memory model in the spirit of Burstall s work Bur72 The Jessie memory model is very efficient for a large variety of well structured C programs However it does not apply when low level memory manip ulations such as heterogeneous casts are involved Moreover Jessie operates by compiling the C program to Why a solution that prevents the user from combining weakest precondition calculus with other techniques such as the Value analysis plug in The WP plug in has been designed with cooperation in mind That is you may use WP for proving some annotation
16. generates concise proof obligations It simply maps each C variable to one pure logical variable However the heap can not be represented in this model and expressions such as p can not be translated at all You can still represent pointer values but you can not read or write the heap through pointers Store model The default model for WP plug in Heap values are stored in a global array Pointer values are translated into an index into this array In order to generate reasonable proof obligations the values stored in the global array are not the machine ones but the logical ones Hence all C integer types are represented by mathematical integers and each pointer type to a given type is represented by a specific logical abstract datatype A consequence is that heterogeneous cast of pointers can not be translated in this model For instance within this memory model you can not cast a pointer to int into a pointer to char and then access the internal representation of an int value in memory 11 CHAPTER 1 INTRODUCTION Runtime model This is a low level memory model where the heap is represented as a wide array of bits Pointer values are exactly translated into memory addresses Read and write operations from to the heap are translated into manipulation of range of bits in the heap This model is very precise in the sense that all the details of the program are represented This comes at the cost of huge proof obligations t
17. hat are very difficult to discharge by automated provers and generally require an interactive proof assistant Thus each memory model offers a different trade off between expressive power and ease of discharging proof obligations The Hoare memory model is very restricted but generates easy proof obligations Runtime is very expressive but generates difficult proof obligations and Store offers an intermediate solution 12 Chapter 2 Using WP Plug in The WP plug in can be used from the Frama C command line or within its graphical user interface It is a dynamically loaded plug in distributed with the kernel since the Carbon release of Frama C This plug in computes proof obligations of programs annotated with ACSL annotations by weakest precondition calculus using a parametrized memory model to represent pointers and heap values The proof obligations may then be discharged by external decision procedures which range over automated theorem provers such as Alt Ergo UCK06 or interactive proof assistant like Coq Coq 10 This chapter describes how to use the plug in from the Frama C graphical user interface section 2 1 from the command line section 2 2 or from another plug in section 2 3 Additionally the combination of the WP plug in with the load and save commands of Frama C and or the then command line option is explained in section 2 4 2 1 Graphical User Interface To use WP under the GUI you simply need to run t
18. haviors b1 bn defaults to all behaviors wp prop lt p gt selects properties with name p defaults to all properties You may also type assigns for all assigns properties wp no status all includes in the goal selection all properties regardless of their current status default is no wp no status valid includes in the goal selection those properties for which the current status is already valid default is no wp no status invalid includes in the goal selection those properties for which the cur rent status is already invalid default is no wp no status maybe includes in the goal selection those properties with an undetermined status default is yes Remark options wp status xxx are not taken into account when selecting a property by its name or from the Gui 2 2 2 Program Entry Point The generic Frama C options dealing with program entry point are taken into account by WP as follows main lt f gt designates f to be the main entry point defaults to main lib entry the main entry point as defined by option main is analyzed regardless of its initial context default is no These options impact the generation of proof obligations for the requires contract of the main entry point More precisely if there is a main entry point and 1ib entry is not set e the global variables are set to their initial values at the beginning of the main entry point for all its pr
19. he Frama C graphical user interface No additional option is required although you can preselect some of the WP options described in section 2 2 frama c gui options c As we can see in figure 2 1 the memory model the decision procedure and some WP options can be tuned from the WP side panel Others options of the WP are still modifiable from the Properties button in the main GUI toolbar To prove a property just select it in the internal source view and chose WP from the contextual menu The Console window outputs some information about the computation Figure 2 2 displays an example of such a session If everything succeeds a green bullet should appear on the left of the property The computa tion can also be run for a bundle of properties if the contextual menu is open from a function or behavior selection The options from the WP side panel correspond to some options of the plug in command line Please refer to section 2 2 for more details In the graphical user interface there are also specific panels that display more details related to WP that we shortly describe below 13 CHAPTER 2 USING WP PLUG IN File Project Analyses Help ca 6 Source file requires valid a a valid b swap c Prove propery by WP 2 25 Sortint int o swap 6 ensures B old b Insert WP safety guards 3 int tmp a swap2 c o assigns a b Insert callee contract 4 a
20. ion computation Consider an annotation Q compute its weakest precondition W across all the statements from Q up to the beginning of the function Then submit the property P gt W to a theorem prover where P are the preconditions of the function If this proof obligation is discharged then one may conclude the annotation Q is valid for all executions Termination We must point out a detail about program termination Strictly speaking the weakest precondition of property Q through statement stmt should also ensure termination and execution without runtime error The proof obligations generated by WP do not entail systematic termination unless you sys tematically specify and validate loop variant ACSL annotations Nevertheless exit behaviors of a function are correctly handled by WP Regarding runtime errors the proof obligations generated by WP assume your program never raises any of them Moreover the only integer model currently implemented assumes no integer overflow at all signed or unsigned As illustrated in the short tutorial example of section 1 2 you should enforce the absence of runtime error on your own for instance by running the value analysis plug in or the rte generation one 10 1 4 MEMORY MODELS Provers The WP plug in computes proof obligations for post conditions and assertions in C functions and submits them to external provers You may discharge the generated proof obligation with automated decision pr
21. lts is 4 processes With wp par 1 the order of logged results is fixed With more processes the order is runtime dependent wp proof lt dp gt selects the decision procedure used to discharge proof obligations See below for supported provers By default alt ergo is selected but you may specify another decision procedure or none to skip the proof step wp proof trace asks for provers to output extra information when available wp timeout lt n gt sets the timeout in seconds for the calls to the decision prover defaults to 10 seconds wp trace keeps user labels in generated proof obligations This option can be useful for tracing where the proof obligations come from especially when using wp split option or interactive proof assistants Alt Ergo Direct support for the Alt Ergo prover is provided You need at least version 0 93 of the prover You select it with wp proof alt ergo option It is also the default selected prover It is still correct to prove these RTE annotations with WP 18 2 2 COMMAND LINE OPTIONS Coq Direct support for the Coq proof assistant is provided The generated proof obligations are accepted by Coq version 8 3 but should also work with prior versions of the proof assistant When working with Coq you will enter interactive session then save the proof scripts in order to replay them in batch mode wp script lt f script gt specifies the file which proof scripts are retrieved from or sav
22. ng memory reads or writes through pointer values because there is no way of representing aliasing You select this memory model in the WP plug in with the option wp model Hoare the analyzer will complain whenever you attempt to access memory through pointers with this model 3 3 Memory Models with Pointers Realistic memory models must deal with reads and writes to memory through pointers How ever there are many ways for modeling the raw bit stream the heap consists of All memory models M actually implement a common signature Pointer Type 7 generally a pair of a base address and an offset Heap Variables for each program point there is a set of logical variables to model the heap For instance you may have a variable for the values at a given address and another one for the allocation table The heap variables m m are denoted by m Read Operation given the heap variables m a pointer value p T and some C type T the model will define an operation readr M p term that defines the representation in of the value of C type T which is stored at address p in the heap Write Operation given the heap variables m before a statement and their associated heap variables m after the statement a pointer value p 7 and a value v of C type T the model will define a relation writer m p v m prop that relates the heap before and after writing value v at address p in the heap 24 3 4 HOARE VARIABL
23. nt aliasing between arguments at call sites e assigns the detected variables passed by reference to the Hoare memory model This optimization is not activated by default since the non aliasing hypotheses at call sites are sometimes irrelevant 26 BIBLIOGRAPHY Bibliography Bur72 R M Burstall Some techniques for proving correctness of programs which alter data structures Machine Intelligence 1972 CCK06 Sylvain Conchon Evelyne Contejean and Johannes Kanig Ergo a theorem prover for polymorphic first order logic modulo theories 2006 Coq10 Coq Development Team The Coq Proof Assistant Reference Manual Version V8 8 2010 Dij68 Edsger W Dijkstra A constructive approach to program correctness BIT Numerical Mathematics Springer 1968 Fil03 J C Filli tre Why a multi language multi prover verification tool Research Report 1366 LRI Universit Paris Sud March 2003 Flo67 R W Floyd Assigning meanings to programs Proceedings of the American Math ematical Society Symposia on Applied Mathematics 19 1967 Hoa69 C A R Hoare An axiomatic basis for computer programming Communications of the ACM 1969 Lei08 K Rustan M Leino This is Boogie 2 Microsoft Research 2008 MMO09 Yannick Moy and Claude March Jessie Plugin Tutorial Beryllium version INRIA 2009 http www frama c cea fr jessie html 27
24. ocedures or an interactive proof assistant Technically WP is interfaced with Alt Ergo CCK06 Coq Coq10 and any decision procedure supported by Why Fil03 1 4 Memory Models The essence of a weakest precondition calculus is to translate code annotation into mathemati cal properties Consider the simple case of an annotation referring to a non pointer C variable x x x 1 assert P x gt 0 We can translate P into the mathematical property P X X gt 0 where X stands for the value of variable x at the appropriate program point In this simple case the effect of statement x x 1 over P is actually the substitution X gt X 1 that is X 1 gt 0 The problem when applying weakest precondition calculus to C programs is to deal with pointers Consider now amp x 3 x 1 assert Q p gt 0 p It is clear that taking into account the aliasing between p and x the effect of the increment of x can not be translated by a simple substitution of X in Q This is where memory models comes to rescue A memory model defines a mapping from values inside the C memory heap to mathematical terms The WP has been designed to support different memory models There are currently three memory models implemented and we plan to implement new ones in future releases Those three models are all different from the one in the Jessie plug in which makes WP complementary to Jessie Hoare model A very efficient model that
25. on Frama C exit see also wp out option The only information which is added to the Frama C kernel consists in a new status for those properties proved by WP with their dependencies Warning the WP plug in does not work yet with several Frama C projects in the same run Thus when combining WP with then save and load options the user should be aware of the following precisions wp wp prop wp fct wp bhv These options make the WP plug in generate proof obligations for the selected properties The value of theses option are never saved and they are cleared by then Hence running wp prop A then wp fct F does what you expect See the plug in development guide 21 CHAPTER 2 USING WP PLUG IN wp print wp proof wp check These options do not generate new proof obligations but run other actions on all previously generated ones For the same reasons they are not saved and cleared by then wp xxx All other options are tunings that can be easily turned on and off or set to the desired value They are saved and kept across then command 22 Chapter 3 WP Models Basically a memory model is a set of datatypes operations and properties that are used to abstract the values living inside the heap during the program execution Each memory model defines its own representation of pointers memory and data actually stored in the memory The memory models also define some types functions and pro
26. operties to be established e special proof obligations are generated for the preconditions of the main entry point hence to be proved with globals properly initialized Otherwise initial values for globals are not taken into account and no proof obligation is generated for preconditions of the main entry point 16 2 2 COMMAND LINE OPTIONS 2 2 3 Model Selection These options modify the underlying memory model that is used for computing weakest preconditions See chapter 3 for details wp model lt m gt sets the memory model among Hoare Store or Runtime For more informa tion about the models and how to choose it see section 1 4 wp no logicvar deactivates optimization for variables whose address is never taken for which WP uses the Hoare model default is yes wp no byreference deactivates detection of arguments passed by reference as point ers for which WP may also use the Hoare model under some hypotheses default is no wp assigns lt m gt sets the method for proving assigns clauses Possible methods are effect Each statement with side effect produces one sub goal The locations written by each statement are checked to be included in the assigns clause This is a stronger result than required but the proof obligations are generally simple and sufficient in practice memory use the ACSL definition of assigns clauses where memory states are com pared before and after the considered block Gene
27. perties required to translate C programs and ACSL annotations into first order logic formule The interest of developing several memory models is to manage the trade off between the precision of the heap s values representation and the difficulty of discharging the generated proof obligations by external decision procedures If you chose a very accurate and detailed memory model you shall be able to generate proof obligations for any program and annota tions but most of them would be hardly discharged by state of the art external provers On the other hand for most C programs simplified models are applicable and will generate less complex proof obligations that are easier to discharge A practical methodology is to use the simpler models whenever it is possible and to up the ante with more involved models on the remaining more complex parts of the code This chapter is dedicated to the description of the memory models implemented by the WP plug in In this preliminary version of the manual we only provide a high level description of the memory models you might select with option wp model section 3 2 and 3 3 Then we focus on two general powerful optimizations The first one activated by default and controlled by option wp no logicvar section 3 4 mixes the selected memory model with the purely logical Hoare model for those parts of your program that never manipulate pointers The second one controled by option wp byreference section 3
28. rates much more complex proof obligations than effect none skip proof of assigns clauses 2 2 4 Computation Strategy These options modifies the way proof obligations are generated during weakest precondition calculus wp invariants computes proof obligations for arbitrary invariants inside loops Also mod ifies the calculus for proper loop invariants This option automatically turns splitting on see wp split wp huge lt s gt cuts off proof terms with size exceeding 2 default 230 The size of a term is linearly related to its size on the disk and to the size of proof obligation sent to decision procedures wp norm lt m gt sets the normalization method applied to let bindings in obligations generated for Alt Ergo and Coq Eqs let bindings are replaced by universally quantified fresh variables with the associ ated defining equalities in hypothesis default Let let bindings are preserved Exp let bindings are expanded To be efficient it is better to put all the loop invariants inside only one annotation Otherwise Frama C insert them at different program points Then the WP cut the generated proof obligations at each invariant instead of proving all of them inside the same induction scheeme Notice that when using the ACSL Importer plug in all the loop invariants are placed at one unique program point and are treated efficiently by WP 17 CHAPTER 2 USING WP PLUG IN Cc let bindings are r
29. s of your C programs and prove other ones with other plug ins The recent improvements of the Frama C kernel are then responsible for managing such partial proofs and consolidate them altogether This manual is divided into three parts This first chapter introduces the WP plug in the Weakest Precondition calculus and Memory Models Then Chapter 2 details how to use and tune the plug in within the Frama C platform Finaly Chapter 3 provides a description for the included memory models CHAPTER 1 INTRODUCTION 1 1 Installation The WP plug in is distributed with the Frama C platform However you must install at least an external prover in order to fulfill proof obligations You have several choices see section 2 2 5 for details To begin with you may install the Alt Ergo UCK06 prover You can install it from source at http alt ergo lri fr or with Godi 1 2 Tutorial Consider the very simple example of a function that swaps the values of two integers passed by reference File swap c void swap int a int b int tmp a a b b tmp returns J A simple although incomplete ACSL contract for this function can be File swap1 c ensures A a old xb ensures B b old xa x void swap int a int b You can run wp on this example with frama c wp swap c swapi c kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swapi c
30. splay a dependency graph for this property The graph displays the property its status which plug in has participated in the proof and on which properties the proof directly depends on 2 2 Command Line Options The best way to know which options are available is to use frama c wp help The WP plug in generally operates in three steps 1 Annotations are selected to produce a control flow graph of elementary statements an notated with hypothesis and goals 2 Weakest preconditions are computed for all selected goals in the control flow graph Proof obligations are emitted and saved on disk 3 Decision procedures provers are run to discharge proof obligations The WP options allow to refine each step of this process It is very convenient to use WP together with the standard then option of Frama C in order to operate successive pass on the project See section 2 4 for details 15 CHAPTER 2 USING WP PLUG IN 2 2 1 Goal Selection This group of options refines the selection of annotations for which proof obligations are generated By default all annotations are selected By default a property which is already proved by WP or any other plug in does not lead to any proof obligation generation wp generates proof obligations for all selected properties wp fct lt f1 fn gt selects annotations of functions f1 fn defaults to all functions wp bhv lt b1 bn gt selects annotation for be
31. wap_assert_4_rte Valid wp Alt Ergo Goal store_swap_assert_3_rte Valid wp Alt Ergo Goal store_swap_assert_2_rte Valid wp Alt Ergo Goal store_swap_assert_1_rte Valid wp Alt Ergo Goal store_swap_post_2_B Valid wp Alt Ergo Goal store_swap_post_1_A Valid We have finished the job of validating this simple C program with respect to its specification as reported by the report plug in that displays a consolidation status of all annotations tt frama c wp verbose O then report kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swap2 c rte annotating function swap report Computing properties status Properties of Function swap Valid Post condition A by WP Store Valid Post condition B by WP Store Valid Assigns file swap2 c line 4 by WP Store Valid Assertion rte generated by WP Store Valid Assertion rte generated by WP Store Valid Assertion rte generated by WP Store Valid Assertion rte generated by WP Store Valid Default behavior by Frama C kernel 8 Completely validated 8 Total 1 3 Weakest Preconditions The principles of weakest precondition calculus are quite simple in essence Given a code anno tation of your program say an assertion Q after a statement stmt the weakest precondition of P is by definition the simplest property P that must be
Download Pdf Manuals
Related Search