WP manual - Frama-C
Contents
1. 26 2 5 Proof Obligation Reports c e sesei aoa Hasena 26 2 6 Plugim Persistent Data occiso a a a a 3 WP Models 3 1 Language of Proof Obligations 3 2 The Hoare Memory Model o o 3 3 Memory Models with Pointers CONTENTS 3 4 Hoare Variables mixed with Pointers aaa 33 3 5 Hoare Variables for Reference Parameters o 33 36 The Typed Memory Model co 0 ooooocmo ocaso 34 WP Simplifier 35 4 1 Logie NormallzaioRsS scos ooo a ae Aw ek ies 35 42 Simpler Engine Qed era 36 43 Eficient WP Computation 6 4 6048586045 dea be eee 37 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 Flo67 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 Y M09 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 separat2. CHAPTER lt per chapter contents gt SECTION lt per section contents of a chapter gt TAIL lt tail contents gt END Configuration section consists of optional commands one per line among CONSOLE the report is printed on standard output Also prints all numbers right aligned on 4 ASCII characters FILE lt file gt the report is generated in file file SUFFIX lt ext gt the report is generated in file base ezt where base can be set with wp report basename option ZERO lt text gt text to be printed for O numbers Default is GLOBAL_SECTION lt text gt text to be printed for the chapter name about globals AXIOMATIC_SECTION lt text gt text to be printed for the chapter name about axiomatics FUNCTION_SECTION lt text gt text to be printed for the chapter name about functions AXIOMATIC_PREFIX lt text gt text to be printed before axiomatic names Default is Axiomatic with a trailing space FUNCTION_PREFIX lt text gt text to be printed before function names Default is empty GLOBAL_PREFIX lt test gt text to be printed before global property names Default is Global with a trailing space LEMMA_PREFIX lt test gt text to be printed before lemma names Default is Lemma with a trailing space OPROPERTY_PREFIX lt text gt text to be printed before other property names The generated report consists of several optional parts corresponding to Head
3. 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 3 2 Program Entry Point The generic Frama C options dealing with program entry point are taken into account by WP plug in 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 lib 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 properties 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 2 3 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 spec gt specify the models to use The specification is a list of selectors Se lectors are usually separated b
4. Chapter and Tail sections of the wp report specification file First the head contents lines are produced Then the chapters and their sections are produced Finally the Tail content lines are printed The different chapters are about globals axiomatics and functions Outputs for these chapters can be specified using these directives CHAPTER lt chapter header gt GLOBAL lt global section contents gt AXIOMATIC lt per ariomat c section contents gt For each axiomatic a specific section is produced under the chapter about axiomatics 28 2 5 PROOF OBLIGATION REPORTS FUNCTION lt per function section contents gt For each function analyzed by WP a specific section is produced under the chapter about functions SECTION lt default section contents gt PROPERTY lt per property contents gt For each property of a section a specific textual contents can be specified Textual contents use special formatters that will be replaced by actual statistics values when the report is generated There are several categories of formatters PO stands for Proof Obligations Formatters Description amp lt col gt insert spaces up to column col amp amp prints a amp hh prints a Y lt stat gt statistics for section prop percentage of finally proved properties in section prop total prop valid prop failed lt prover gt lt prover gt lt stat gt number of covered properties
5. 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 A readint Mm P Next the model retrieves the previous int value at actual address Ap say Vp Vp readint M Ap Finally the model relates the final memory state m with the incremented value V 1 at address P writeint Ap Vp 1 7 3 4 Hoare Variables mixed with Pointers As illustrated above a very simple statement is generally translated by memory models into complex formule However it is possible 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 po
6. 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 6 15 CHAPTER 2 USING WP PLUG IN 2 1 Installing Provers The WP plug in requires external provers to work The natively supported provers are Prover Version Download Alt Ergo 0 95 2 http alt ergo ocamlpro com CCKO06 Coq 8 4 pl 12 http coq inria fr Coq10 Why3 0 81 http why3 1ri fr BFMP11 Other provers like Gappa Z3 CVC3 CVC4 PVS and many others are accessible from WP throught Why3 We refer the user to the manual of Why3 to handle specific configuration tasks Provers can be installed at any time before or after the installation of Frama C WP However when using Coq and Why 3 it is better to install them before or to re configure and re install WP as explained below Configuration When using Coq and Why 3 pre compiled libraries are built during com pilation of Frama C which speed up the proof process in a significant way This behavior can be turned on off at configure time typically configure disable wp coq disable wp why3 Compilation If you want to compile the Coq and Why 3 libraries manually you can still run make wp coq wp why3 tt sudo make wp coq install Remark The Why Fil03 prover is no more supported since WP version 0 7 16 2 2 GRAPHICAL USER INTERFACE 2 2 Graphical User Interface To use W
7. Hence all C integer types are represented by 11 CHAPTER 1 INTRODUCTION mathematical integers and each pointer type to a given type is represented by a specific logical abstract datatype A consequence of having separated arrays 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 the original int value into memory However variants of the Typed model enables limited forms of casts See chapter 3 for details Bytes model Not Implemented Yet This is a low level memory model where the heap is represented as a wide array of bytes 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 that 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 Bytes is very expressive but generates difficult proof obligations and Typed offers an intermediate solution Chapter 3
8. 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 that consists of e Natural signed unbounded integer constants and their operations e Natural real numbers and their operations e Arrays as total maps and records tuples with named fields e Abstract polymorphic data types 31 CHAPTER 3 WP MODELS e Anonymous function symbols with optional algebraic properties e 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 x before the statement and x2 after the statement with the obvious relation xz x 1 if no overflow occurred Of course this model is not capable of handling memory reads or writes thr
9. function If this proof obligation is discharged then one may conclude the annotation Q is valid for all executions 10 1 4 MEMORY MODELS 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 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 and proving the generated assertions 1 4 Memory Models The essence of a weakest precondition calculus is to translate code annotation into mathemat ical properties Consider the simple case of a property about an integer C variable x x x 1 assert P x gt 205 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 appl
10. string to the current value of the option The following options are defined by the plugin coq file altergo file why3 file and why3 import C Comments are allowed in the file For overloaded ACSL symbols it is necessary to provide one link symbol for each existing signature The same link symbol is used for all provers and must be defined in the specified libraries or in the external ones see 2 3 9 It is also possible to specify different names for each prover with the following syntax coq a altergo b why3 c Alternatively a link name can be an arbitrary string with patterns substituted by arguments 1 When a library lib is specified the loaded module depend on the target solver 25 CHAPTER 2 USING WP PLUG IN Option Format Coq coq file dir path v Alt Ergo altergo file path mlw Why3 why3 file path why namel as why3 import theoryl as Precise meaning of formats is given by the following examples all filenames are relatives to the driver file s directory coq file mydir bar v Imports module Bar from file mydir bar vo coq file mydir foo Foo v Loads coq library foo Foo from file mydir foo Foo vo why3 file mydir foo why Imports theory foo Foo from directory mydir why3 file mydir foo why Bar Imports theory foo Bar from directory mydir why3 file mydir foo why Bar T Imports theory foo Bar as T from directory mydir why3 import foo Bar Imports theory foo Bar with no additiona
11. 3 9 Additional Proof Libraries It is possible to add additional bases of knowledge to decision procedures This support is provided for Alt Ergo Why3 and Coq thanks to the following options wp share lt dir gt modifies the default directory where resources are found This option can useful for using a modified or patched distribution of WP wp include lt dir sharedir gt deprecated use driver instead sets the directories where external libraries and driver files are looked for The current directory implicitly added to that list is always looked up first Relative directory names are relative to the current directory except for names prefixed by the characters In such a name the directory is relative to the main FRAMAC_SHARE directory 24 2 3 COMMAND LINE OPTIONS wp alt ergo lib lt f gt deprecated use altergo file in driver instead looks for Alt Ergo library files f ml1w and inlines them into the proof obligation files for Alt Ergo wp cog lib lt f gt deprecated use coq file in driver instead looks for Coq files v or f vo If f vo is not found then WP copies f v is copied into its working directory see option wp out and compiles it locally wp why lib lt f gt deprecated use why3 file in driver instead looks for Why3 library file why and open the library f F for the proving the goals 2 3 10 Linking ACSL Symbols to External Libraries In addition to additional proof l
12. P plug in under the GUI you simply need to run the Frama C graphical user interface No additional option is required although you can preselect some of the WP options described in section 2 3 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 plug in 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 choose WP from the contex tual 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 3 for more details In the graphical user interface there are also specific panels that display more details related to WP plug in that we shortly describe below 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 plu
13. PLUG IN There is a limited support for triggers in WP The sub terms and sub predicates marked with label TRIGGER in an axiom or lemma are collected to generate a multi trigger for their associated free variables 2 3 6 Qed Simplifier Engine These options control the simplifications performed by the WP plug in before sending proof obligations to external provers wp no simpl simplifies constant expressions and tautologies default is yes wp no clean removes unused terms and variables from proof obligations default is yes wp no let propagates equalities by substitutions and let bindings default is yes wp no pruning eliminates trivial branches of conditionals default is yes wp no bits simplifies bitwise operations default is yes 2 3 7 Decision Procedures Interface The generated proof obligations are submitted to external decision procedures If proof obli gations 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 to external decision procedures wp prover lt dp gt selects the decision procedures used to discharge proof obligations See below for supported provers By default alt ergo is selected but you may specify another decision procedure or a list of to try with Finally you should supply none for this option to skip the proof step It is possible to ask for several deci
14. Software Analyzers WP 0 8 WP Plug in Manual Version 0 9 for Sodium 20150201 Patrick Baudin Francois Bobot Loic Correnson Zaynah Dargaye CEA LIST Software Safety Laboratory February 2015 2010 2015 CEA LIST This work has been supported by the U3CAT ANR project Contents 1 Introduction 7 LL Installation axones ah a ee a a ch 12 Tutorial ye ums wurden a a a ate ea ewe Se ge a Re a a 8 1 3 Weakest Preconditions oe c cc gusi poa sar eu Kran aan ae ee ae 10 1 2 Memory Models a2 6 hehe Rasa ea RA es 11 1 5 Ar ihmelies Modelo s a dus u 44 6 4 wt ae be haha A a a ed alas 13 2 Using WP Plug in 15 2 1 Inptalling PROVEE o c 44 eee rara wine Ped ee EA 16 2 2 Graphical User Interface 2 2 24 2a eR a a RR a eS 17 2 Command bine Options ur u 00 Ya ae ee na ad 19 23 1 Goal Selection lt sa sanoe 008 02 Bb ede ree ee rar 19 2 3 2 Program Entity Ponte re oes oS 2G Ped eee ee Gwe Ba 20 2 38 Model Selection v eau sawa uor eee ek ho be dann 20 294 Computation Strategy coccion ne ea aaa 21 Yow reger Generation Gs sl au ta he ae Goa g 21 2 3 6 Qed Simplifier Engine Eon nn 22 2 3 7 Decision Procedures Interface CK 2 une 22 2 3 8 Generated Proof Obligations 2 lt lt o 24 2 3 9 Additional Proof Libraries 2 2 mE nme nenn 24 2 3 10 Linking ACSL Symbols to External Libraries 25 2 4 Plug in Developer Interface o o
15. aive weakest precondition of the conditional is E Wa WB With this formula the weakest preconditions of the program after the conditional is duplicated inside Wa and Wg Moreover this common post conditions have been transformed by the effects of A and B Then the factorization of common sub terms of logic language is not capable of avoiding the duplication In presence of successive conditionals proof obligations generated become twice as big at each conditional statement To tackle this problem the solution is to put the program in passive form FS01 Lei03 Each variable of the program is assigned a different logic variable in each branch The different variables are joined at conditionals into new fresh variables and equality conditions In practice the passive form transformation is done during the weakest precondition calculus together with the translation of C and ACSL by the memory model Hence a translation map co is maintained at each program point from memory model variables to logic variables Joining to maps o and oa from the branches of a conditional leads to a new map o assigning a new logic variable x to memory variable m whenever o1 m and oa m are different This join also produces the two sets of equalities H and Ha associated to this variables renaming Hence o m o m below is member of H and o m oa m is member of Ha Now if W is the post condition of the conditional program below W4 and Wg
16. ation and com mutation of memory accesses and updates Store Memory In the Store memory model the heap is represented by one single memory variable holding an array of data indexed by addresses Then integers floats and pointers must be boxed into data and unboxed from data to implement read and write operations These boxing unboxing operations typically prevent Alt Ergo from making maximal usage of lts native array theory Typed Memory Inthe Typed memory model the heap is now represented by three memory variables holding respectively arrays of integers floats and addresses indexed by addresses This way all boxing and unboxing operations are avoided Moreover the native array theory of Alt Ergo works very well with its record native theory used for addresses memory variables access update commutation can now rely on record theory to decide that two addresses are different separated 34 Chapter 4 WP Simplifier The logical language used to build proof obligations is now equipped with build in sim plifications This allows for proof obligations to be simplified before being sent to external provers and sometimes to be reduced to trivial goals This chapter is dedicated to the description of simplifier and how to use it with WP plug in It also present how combinatorial explosion of path exploration is now tackled down thanks to passive form transformation and automated sub terms factorization FS01 Lei03 This also lead
17. can always be decomposed into WA w9 AW and Wg We AW Finally the weakest precondition of the conditional is E HAWS H2AW2 AW This form actually factorizes the common postcondition to A and B which makes the weakest precondition calculus linear into the number of program statements 37 BIBLIOGRAPHY Bibliography BFMP11 Francois Bobot Jean Christophe Filli tre Claude March and Andrei Paskevich Bur72 Why3 Shepherd your herd of provers First International Workshop on Intermediate Verification Languages August 2011 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 Coq10 Dij68 Fi103 F1067 FSo1 Hoa69 Lei03 Leios MM09 for polymorphic first order logic modulo theories 2006 Coq Development Team The Coq Proof Assistant Reference Manual Version V8 4 2010 Edsger W Dijkstra A constructive approach to program correctness BIT Numerical Mathematics Springer 1968 J C Filli tre Why a multi language multi prover verification tool Research Report 1366 LRI Universit Paris Sud March 2003 R W Floyd Assigning meanings to programs Proceedings of the American Math ematical Society Symposia on Applied Mathematics 19 1967 Cormac Flanagan and James B Saxe Avoiding Exponential Explos
18. data is stored on disk before being sent to provers and they are stored in a temporary directory that is removed upon 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 plug in with their dependencies Thus when combining WP options 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 values of theses options are never saved and they are cleared by then Hence running wp prop A then wp fct F does what you expect properties tagged by A are proved only once wp print wp prover wp gen wp detect 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 30 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 a
19. del Qed Alt Ergo Coq Why3 steps 0 Depth o Timeout 10 El proces la E Post condition B Typed D Slicing swap Assigns 1 3 Typed gt impact swap Assigns 2 3 Typed gt Occurrence swap Assigns 3 3 Typed gt Value gt Metrics Figure 2 2 WP run from the GUI 18 2 3 COMMAND LINE OPTIONS 2 3 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 them together with the standard then option of Frama C in order to operate successive pass on the project See section 2 6 for details 2 3 1 Goal Selection This group of options refines the selection of annotations for which proof obligations are generated By default all annotations are selected A property which is already proved by WP or by any other plug in does not lead to any proof obligation generation unless the pr
20. e proof obligation to prevent your program from raising a runtime error because this property may be validated with any other techniques for instance by running the value analysis plug in or the rte generation one Alt Ergo http alt ergo lri fr 1 2 TUTORIAL Hence consider the following new contract for swap File swap2 h requires valid a amp amp valid b Q ensures A xa old xb ensures B xb old xa assigns a x xb Ox 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 frama c wp wp rte swap c swap2 h kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swap2 h wp Running WP plugin wp Collecting axiomatic usage rte annotating function swap wp 9 goals scheduled wp A1t Ergo Goal typed_swap_post_A Valid 15 wp Qed Goal typed_swap_post_B Valid wp Alt Ergo Goal typed_swap_assert_rte_mem_access Valid 17 wp Qed Goal typed_swap_assert_rte_mem_access_2 Valid wp Alt Ergo Goal typed_swap_assert_rte_mem_access_3 Valid 17 wp Qed Goal typed_swap_assert_rte_mem_access_4 Valid wp Qed Goal typed_swap_assign_parti Valid wp Alt Ergo Goal typed_swap_assign_part2 Valid 22 wp Alt Ergo Goal typed_swap_assign_part3 Valid 22 wp Proved goals 9 9 Qed 4 Alt Erg
21. ely unsound with respect to C and IEEE semantics There is no way of recovering a correct or partial property from the generated proof obligations on floating point operations with this model Float Model floating point operations are defined to be the mathetical ones with a rounding operation This is fully consistent with the IEEE semantics Most automated provers are not able to discharge the generated proof obligations Special support for the Gappa theorem prover is available through Why3 By default the WP plug in uses the Natural model for integers and the unsound Real model for floating points 13 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 CCK06 interactive proof assistant like Coq Coq10 and the interactive proof manager Why3 BFMP11 This chapter describes how to use the plug in from the Frama C graphical user interface section 2 2 from the command line section 2 3 or from another plug in section 2 4
22. en after running stmt Q holds 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 r 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 iQ Introducing W wp f Q we have by definition of wp W f Q Suppose now that we can prove that precondition P entails weakest precondition W we can then conclude that P precondition of f always entails its postcondition Q This proof can be summarized by the following diagram FW Wifi P Q This is the main idea of how to prove a property by weakest precondition 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 W toa theorem prover where P are the preconditions of the
23. en the goal is not proved wp steps lt n gt sets the maximal number of Alt Ergo steps This can be used as a machine independant alternative to timeout wp depth lt n gt sets stop and age limite parameters of Alt Ergo such that n cycles of quan tifier instantiations are enabled wp alt ergo opt lt opt gt passes additional options to Alt Ergo default none Coq Direct support for the Coq proof assistant is provided The generated proof obligations are accepted by Coq version 8 4 When working with Coq you will enter interactive session then save the proof scripts in order to replay them in batch mode wp prover coq runs coqc with the default tactic or with the available proof script see below wp prover 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 As soon as coqide exits the edited proof script is saved back see below and finally checked by coqgc The only part of the edited file retained by WP is the proof script between Proof Qed wp script lt f script gt specifies the file which proof scripts are retrieved from or saved 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 no update script if turned off the user
24. expression is simplified before simplifying each branch under the appropriate hypothesis TE Hp HT TOH EK ADA re H H Bp B TE H A B gt H A B Inside the WP plug in the proof contexts are only build in terms of conjunctions conditional and inference rules Hence these laws are sufficient to perform proof context simplifications Technically simplification has a quadratic complexity in the width and depth of the proof formula Options will be added to control the risk for combinatorial explosion In practice simplification is delayed until submission of the proof obligation to external provers that have similar complexity Since we account on simplification for enhancing prover efficiency we expect this extra cost to be valuable The power of the simplification process depends on the simplification plug ins loaded in the Qed engine and will be the purpose of further developments 36 4 3 EFFICIENT WP COMPUTATION 4 3 Efficient WP Computation During the Weakest Precondition calculus proof obligations are constructed backwardly for each program instruction Conditional statements are of particular interest since they intro duce a fork in the generated proof contexts More precisely consider a conditional statement if e A else B Let Wa be the weakest precondition calculus from block A and Wg the one from block B Provided the transla tion of expression e in the current memory model leads to assumption E the n
25. f 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 selector wp model ref and the necessary separation conditions are generated on the fly This memory model first detects pointer or array variables that are always passed by reference The detected variables are then assigned to the Hoare memory model This optimization is not activated by default since the non aliasing assumptions at call sites are sometimes irrelevant 3 6 The Typed Memory Model This memory model is actually a reformulation of the Store memory model used in previous versions of the WP plug in In theory its power of expression is equivalent However in practice the reformulation we performed makes better usage of built in theories of Alt Ergo theorem prover and Coq features The main modifications concern the heap encoding and the representation of addresses Addresses We now use native records of and provers to encode addresses as pairs of base and offset integers This simplify greatly reasoning about pointer separ
26. g in are Icons for properties O No proof attempted The property has not been validated The property is valid but has dependencies A The property and all its dependencies are valid Proof Obligations Panel This panel is dedicated to the WP plug in It shows the gen erated proof obligations and their status for each prover By double clicking an annotation you can view its mathematical definition in a human readable format By clicking on a prover column you can also submit a proof obligation to a prover by hand Right click provides more option depending on the prover such as proof script editing for Coq 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 display 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 17 CHAPTER 2 USING WP PLUG IN X Frama C 000 File Project Analyses Help a D El ra Exit Source files Reparse Load session Save session Back Forward Analyses Stop Source file swap c 1 void swa
27. ibraries it is also possible to link declared ACSL symbols to external or predefined symbols In such a case the corresponding ACSL definitions if any are not exported by WPs External linkage is specified in driver files It is possible to load one or several drivers with the following WP plug in option wp driver lt file gt load specified driver files see section 2 3 9 Each driver file contains a list of bindings with the following syntax library lib lib lib group field string group field string type symbol link ctor type symbol type type link logic type symbol type type property tags link predicate symbol type type link It is also possible to define aliases to another ACSL symbols rather than external links In this case you may replace by and use an ACSL identifier in place of the external link No property tag is allowed when defining aliases Library specification is optional and applies to subsequent linked symbols If provided the WP plug in automatically load the specified external libraries when linked symbols are used in a goal Dependencies among libraries can be specified also after the The generic group field options have a specific value for each theory The binding applies to the current theory The binding with the operator reset the option to the singleton of the given string and the binding with the operator add the given
28. inters 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 selector wp model raw 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 o 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 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 33 CHAPTER 3 WP MODELS Hence not only can a and b be managed by the Hoare model but we can also treat xa 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 1 y 2 swap amp x amp y Strictly speaking this program takes the addresses o
29. ion Generating Compact Verification Conditions In Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages pages 193 205 ACM January 2001 C A R Hoare An axiomatic basis for computer programming Communications of the ACM 1969 K Rustan Leino Efficient weakest preconditions 2003 K Rustan M Leino This is Boogie 2 Microsoft Research 2008 Yannick Moy and Claude March Jessie Plugin Tutorial Beryllium version INRIA 2009 http www frama c cea fr jessie html 39
30. ion 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 annotations 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 Chapter 3 provides a description for the included memory models Finally we present in Chapter 4 the simplifier module and the efficient weakest precondition engine implemented in WP plug in CHAPTER 1 INTRODUCTION 1 1 Installation The WP plug in is distributed with the Frama C platform However you should install at least one external prover in order to fulfill proof obligations An easy choice is to install the Alt Ergo theorem prover developped at INRIA See
31. is dedicated to a more detailed description of memory models and how the WP plug in use and combine them to generate efficient proof obligations Remark The original Store and Runtime memory models are no more available since WP version 0 7 the Typed model replaces the Store one the Runtime model will be entirely re implemented as Bytes model in some future release 12 1 5 ARITHMETICS MODELS 1 5 Arithmetics Models The WP plug in is able to take into account the precise semantics of integral and floating point operations of C programs However doing so generally leads to very complex proof obligations For tackling this complexity the WP plug in rely on several arithmetic models Natural Model integer operations are performed on mathematical integers Conversions between different integer types are still translated with modulo though Generated proof obligations with this model are well supported by state of the art provers But the C operations must never overflow for the proof obligations to be correct This can be verified aside by running RTE plug in with specific options or with the wp rte option Machine Integer Model integer operations are always performed with modulo This model removes the constraint of generating the guards against overflows But the generated proof obligations are generally difficult to discharge Real Model floating point operations are transformed on real with no rounding This is complet
32. l includes why3 import foo Bar T Imports theory foo Bar as T with no additional includes See also the default WP driver file in wp share wp driver Optional property tags can be given to logic link symbols to allow the WP to performs additional simplifications See section 4 Tags consists of an identifier with column sometimes followed by a link link The available tags are depicted on figure 2 3 2 4 Plug in Developer Interface The WP plug in has several entry points registered in the Dynamic module of Frama C All the entry points are documented in the Frama C html documentation in the Wp API page of the plug in section 2 5 Proof Obligation Reports The WP plug in can export statistics on generated proof obligations These statistics are called WP reports and are distinct from those property reports generated by the Report plug in Actually WP reports are statistics on proof obligations generated by WP whereas property reports are consolidated status of properties generated by Frama C kernel from various ana lyzers We only discuss WP reports in this section Reports are generated with the following command line options wp report lt Rspec Rspec gt specifies the list of reports to export Each value Rspec is a WP report specification file described below wp report basename lt name gt set the basename for exported reports described below See the plug in deve
33. lopment guide 26 2 5 PROOF OBLIGATION REPORTS Tags Operator Properties commutative specify a commutative symbol rOy yOx associative specify an associative symbol x4 y z 2 y z ac shortcut for associative commutative left balance the operator on left during export to solvers requires the associative tag 1OyOz 10y O z right balance the operator on right during export to solvers re absorbant a link neutral e link quires the associative tag rOyOz 2 yO 2 specify a link as being the absorbant element of the sym bol a link x a link x a link a link specify e link as being the neutral element of the symbol e link Ox x O e link x inversible specify simplification relying on the existence of an inverse TOY 202 gt Y 2 YOr 20t gt y 2 idempotent specify an idempotent symbol x O x x injective specify an injective function fircan Wie gt Vz Y constructor specify an injective function that construct different values from any other constructor Formally whenever f and g are two distinct constructors they are both injective and z1 En 7 MI forall z and yj Figure 2 3 Driver Property Tags 27 CHAPTER 2 USING WP PLUG IN Reports are created from user defined wp report specification files The general format of a wp report file is as follows lt configuration section gt CHEAD lt head contents gt
34. malizing logic language we have a simplifier engine named Qed The simplifier engine is used by WP plug in to simplify the generated proof contexts and proof obligations The basic feature of Qed is to manage a base of knowledge T It is possible to add new facts hypotheses to T and to simplify rewrite a term of a property with respect tor By default the only rewriting performed by Qed is the propagation of equality classes by normalization The Qed engine can be enriched by means of plug ins to perform more dedi cated simplifications For instance we have developed a simplifier plug in for array and record theories and a prototype for linear inequalities WP uses the simplification engine to simplify proof contexts by recursively combining for basic laws involving the simplifier engine Each law is applied with respect to a local base of knowledge T initially empty Adding a new fact H toT is denoted by T H rewriting a term of predicate e into e with respect to T is denoted by T j eve Inference Law An hypothesis is simplified and added to the knowledge base to simplify the goal FEA T HEGprG TE H gt G gt HG Conjunction Law Each side of a conjunction is simplified with the added knowledge of the other side This law scales up to the conjunction of n facts and simplifications can be performed incrementally T 8 BF A gt T eAE Bros TE AAB pb A A B Conditional Law The conditional
35. nd properties required to translate C programs and ACSL annotations into first order logic formula 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 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 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 section 3 5 is dedicated to those pointers that are formal parameters of function passed by reference 3 1
36. number of finally proved properties number of remaining unproved properties discharged PO by prover statistics for prover in section Provers lt prover gt A prover name see wp prover Statistics lt prover gt total valid failed time steps success number of generated PO number of discharged PO number of non discharged PO maximal time used by prover for one PO maximal steps used by prover for one PO percentage of discharged PO Remarks amp ergo is a shortcut for amp alt ergo Formatters can be written or At Textual contents can use naming formatters that will be replaced by current names 29 CHAPTER 2 USING WP PLUG IN Names Description chapter current chapter name section current section name global current global name under the chapter about globals haxiomatic current axiomatic name under the chapter about axiomatics function current function name under the chapter about functions name current name defined by the context property name inside PROPERTY contents function name inside FUNCTION contents axiomatic name inside AXIOMATIC contents global name inside GLOBAL contents section name inside SECTION contents chapter name inside CHAPTER contents 2 6 Plug in Persistent Data As a general observation hardly none of the internal WP data is kept in memory after each execution Most of the generated proof obligation
37. o 5 22 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 frama c wp verbose O then report kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swap2 h rte annotating function swap report Computing properties status Valid Post condition A by Wp typed Valid Post condition B by Wp typed Valid Assigns file swap2 h line 4 by Wp typed Valid Assertion rte mem_access file swap c line 3 by Wp typed Valid Assertion rte mem_access file swap c line 4 by Wp typed Valid Assertion rte mem_access file swap c line 4 by Wp typed Valid Assertion rte mem_access file swap c line 5 by Wp typed Valid Default behavior by Frama C kernel 8 Completely validated 8 Total CHAPTER 1 INTRODUCTION 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 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 th
38. operty is individually selected from the graphical user interface of the programmatic API wp generates proof obligations for all selected properties wp fct lt f f gt selects annotations of functions f1 fn defaults to all functions wp skip fct lt f f gt remove annotations of functions f1 fn defaults to none wp bhv lt b b gt selects annotation for behaviors bj b defaults to all behaviors of the selected functions wp prop lt pi Pn gt selects properties having p or pn as tagname defaults to all prop erties You may also replace a tagname by a lt category gt of properties Recognized categories are Olemma Grequires Qassigns Oensures exits Qassert invariant Qvariant Obreaks Ocontinues Oreturns complete_behaviors disjoint_behaviors Properties can be prefixed with a minus sign to skip the associated annotations For ex ample wp prop assigns removes all assigns and loop assigns properties from the selection 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 19 CHAPTER 2 USING WP PLUG IN wp no
39. ough 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 my 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 ready Mm p term that defines the representation in of the value of C type T which is stored at address pin 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 Mm p v m prop that relates the heap before and after writing value v at address p in the heap 32 3 4 HOARE VARIABLES MIXED WITH POINTERS
40. p int a int b 21 3 int tmp a 4 ta b a 5 b tmp on annota 6 return Insert WP safety guards 7 Insert all callees contract a al Enable slicing Dependencies gt Callers Y WP Model Typed Script None ka At Ergo A 2 Information Messages Console Properties WP Goals This is the declaration of function swap ORE O Split O Trace I Proof It is referenced and its address is not taken O Invariants Steps o 5 Depth o pl Timeout 10 5 Process la gt Slicing D Impact gt Occurrence gt Value gt Metrics IE v Figure 2 1 WP in the Frama C GUI Eile Project Analyses Help a D 8 El N Exit Source files Reparse Load session Save session Back F rd Analyses Stop Te Bre requires valid a a valid b swap c ensures A old a old b o ensures B old b old a 1 void swap int a int b e assigns a b Bi 3 int tmp a void swap int a int b 4 a b 5 b tmp int tmp 6 return tmp a 7 a b 8 b tmp return V WP Model Typed Script None Information Messages Console Properties WP Goals Provers Alt Ergo native a ORE O Split C Trace I Proof E Al Module Property tieli O Invariants Module Goal Mo
41. s script file will not be modified A warning is emitted if script data base changed wp tactic lt ltac gt specifies the Coq tactic to try with when no user script is found The default tactical is auto with zarith See also how to load external libraries and user defined tactics in section 2 3 9 wp tryhints When both the user provided script and the default tactic solve the goal other scripts for similar goals can be tried instead wp hints lt n gt sets the maximal number of suggested proof scripts wp coq timeout lt n gt sets the maximal time in seconds for running coqc checker Does not apply to coqide default 30s wp cog opt lt opt gt additional options for coqc and coqide default none 23 CHAPTER 2 USING WP PLUG IN Why3 Since WP version 0 7 native support for Why3 and Why3 Ide are provided The older system Why 2 x is no more supported wp prover why3ide runs Why Ide with all generated goals On exit the WP plug in reads back your Why3 session and update the proof obligation status accordingly wp prover lt p gt runs a Why3 prover named lt p gt wp prover why3 lt p gt useful alias when lt p gt can be ambiguous It is actually different to run alt ergo or coq directly from WP or through Why3 wp detect lists the provers available with Why3 This command calls why3 list provers but you have to configure Why3 on your own before for instance by using why3config Consul
42. s to more compact and somehow more readable proof obligations with less memory less disk usage and lower external prover time overhead compared to WP versions 0 6 and lower 4 1 Logic Normalizations The new logic language is naturally equipped with term normalization and maximal sub term sharing It is only used with new memory models not with the standard ones The maximal sub term sharing are responsible for the introduction of let bindings whenever a sub expression appears several times in the generated proof obligations The occupied memory and disk usage of WP is also reduced compared to other models The normalization rules can not be turned off and are responsible for local simplifications Although modest they can turn a proof obligation to be trivialy discharged Logic normalization by commutativity and associativity absorption and neutral elements elimination of redundant facts propagation of negations Morgan laws simplification of conditionals Arithmetic normalization by commutativity and associativity absorption and neutral el ements factorization with linear forms constant folding normalization of linear equalities and inequalities Array elimination of consecutive access and updates Record elimination of consecutive access and updates simplification of structural equalities and inequalities 35 CHAPTER 4 WP SIMPLIFIER 4 2 Simplifier Engine Qed Build on top of our nor
43. section 2 1 for installing other provers 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 returni lt A simple although incomplete ACSL contract for this function can be File swap1 h ensures A a old b ensures B xb old xa void swap int a int b You can run wp on this example with frama c wp swap c swapi h kernel preprocessing with gcc C E I swap c kernel preprocessing with gcc C E I swapi h wp Running WP plugin wp Collecting axiomatic usage wp warning Missing RTE guards wp 2 goals scheduled wp Alt Ergo Goal typed_swap_post_A Valid 10 wp Qed Goal typed_swap_post_B Valid wp Proved goals 2 2 Qed 1 Alt Ergo 1 10 As expected running WP for the swap contract results in two proof obligations one for each ensures clause The first one is discharged internally by the Qed simplifier of WP the second one is terminated by Alt Ergo You should notice the warning Missing RTE 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 generat
44. sion procedures to be tried For each goal the first decision procedure that succeed cancels the other attempts wp proof lt dp gt deprecated alias for wp prover for backward compatibility with WP version 0 6 wp gen only generates proof obligations do not run provers See option wp out to obtain the generated proof obligations wp par lt n gt limits the number of parallel process runs for decision procedures Defaults is 4 processes With wp par 1 the order of logged results is fixed With more processes the order is runtime dependent wp filename truncation lt n gt truncates basename of proof obligation files to n charac ters Since numbers can be added as suffixes to make theses filenames unique filename lengths can be highter to n No truncation is performed when the value equals to zero wp no proof trace asks for provers to output extra information on proved goals when available default is no wp no unsat model asks for provers to output extra information when goals are not proved default is no 22 2 3 COMMAND LINE OPTIONS wp timeout lt n gt sets the timeout in seconds for the calls to the decision prover defaults to 10 seconds Alt Ergo Direct support for the Alt Ergo prover is provided You need at least version 0 95 of the prover It is also the default selected prover wp prover alt ergo selects Alt Ergo wp prover altgr ergo opens the graphical interface of Alt Ergo wh
45. t the Why3 user manual for details The listed prover names can be directly used with wp prover option Sessions Your Why3 session is saved in the project session sub directory of wp out You may run why3ide by hand by issuing the following command why3ide I lt frama c share gt wp lt out gt project session Proof recovering features of Why3 are fully available and you can interleave proving from WP with manual runs of why3ide Interactive proofs with Why3 are completely separated from those managed by the native WP interface with Coq 2 3 8 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 no print pretty prints the generated proof obligations on the standard output Re sults obtained by provers are reported as well default is no 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 2
46. tes RTE guards before computing weakest preconditions This op tion calls the rte generation plug in with the following options rte mem rte div warn signed overflow and warn unsigned overflow The generated guards when proved fulfill the requirements for using the WP plug in with natural integer domain default is no wp no split conjunctions in generated proof obligations are recursively split into sub goals The generated goal names are suffixed by part lt n gt defaults to no wp no invariants computes proof obligations for arbitrary invariants inside loops Also modifies the calculus for proper loop invariants default is no 2 3 5 Trigger Generation The ACSL language does not provide user with syntax for declaring triggers associated to lemmas and axioms However triggers are generally necessary for SMT solvers to discharge efficiently the generated proof obligations t is still correct to prove these RTE annotations with WP plug in 2To 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 calculus cuts the generated proof obligations at each invariant instead of proving all of them inside the same induction scheme 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 plug in 21 CHAPTER 2 USING WP
47. y although other separators are accepted as well _ spaces newlines tabs and parentheses 9 Selectors are case insensitive The option wp model can be used several times All pro vided selectors are processed from left to right potentially reverting previous selectors The available selectors are 20 2 3 COMMAND LINE OPTIONS Selector Description Hoare Select Hoare memory model Typed Select Typed memory model with limited casts cast Select Typed memory model with unlimited casts unsound nocast Select Typed memory model with no casts raw Disable the combination of memory models var Combination of memory models based on variable analysis ref Activate the detection of pointer variables used for reference passing style nat Use natural integer model no overflows int Use machine integers modulo arithmetics cint alias for int real Use mathematical reals instead of floating points float Use floating point operations cfloat alias for float Default settings corresponds to wp model Typed var nat real wp literals exports the contents of string literals to provers default no wp extern arrays gives an arbitrary large size to arrays with no dimensions This is a modelization of infinite size arrays default is no 2 3 4 Computation Strategy These options modifies the way proof obligations are generated during weakest precondition calculus wp no rte genera
48. ying weakest precondition calculus to C programs is to deal with pointers Consider now Re x 1 Q 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 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 Typed model The default model for WP plug in Heap values are stored in several separated global arrays one for each atomic type integers floats pointers and additional one for memory allocation Pointer values are translated into an index into these arrays In order to generate reasonable proof obligations the values stored in the global array are not the machine ones but the logical ones
Download Pdf Manuals
Related Search