The Extended Design And Implementation Of Shape System Of Safe C Language Verifier

With the development of computer technology,nowadays,software has already been integrated into people's daily life and work.While the scalability and complexity of software has increased significantly,the quality of software is still less than satisfac-tory,and the accidents caused by software are threatening in safety-critical domains.Improving the reliability of software is a general trend,and one of the main research directions is formal verification based on deductive reasoning.Our research group has designed and developed a program verifier for the Safe C language.It is based on deductive reasoning and applies Hoare logic and Shape Graph logic.In particular,the shape system as one component of the verifier is the imple-mentation of the Shape Graph logic,which can be used to perform the computation for statements related to heap memory and to restrict the mutable data structures which can be used by programs,as well as their operations.This work applies a series of improve-ments and extensions to the prototype of the shape system to overcome its drawbacks.First,this work extends the calculation operation of the shape system.This work introduces several operation rules for superscript expressions,so the calculation of node locating can cover the case of pointer access paths with superscript,which has better ion ability.In addition,this work utilizes the window of function invocation,to refine and implement the rule of function invocation calculation,which is the most complex one of Shape Graph logic.With this rule,the shape system can perform the computation for function call statements correctly.Second,this work improves the shape graph generation approach.The shape graph generation approach can create equivalent shape graphs with assertions,which describe information of heap pointers.Only with generated shape graphs,can the shape system performance the computation for heap pointer related statements normally.This work introduces built-in shape predicates to simplify and reuse assertions.Operation seman-tics are also applied to different kinds of assertions,so that the shape system can create shape graphs accurately and errors in assertions can be detected.Furthermore,this work introduces an approach for deducing built-in predicates from customized predicates,in order to avoid the problem of redundancy in assertions caused by built-in shape predi?cates.Third,this work introduces a shape checking approach.The shape checking ap-proach can be used to check whether or not mutable data structures conform to def-initions of Safe C language.Three shape levels are introduced to represent different checking levels of rigor.In order to reduce the complexity caused by different pointer field types of mutable data structures,this approach utilizes a three-phase processing framework:shape splitting,shape analysis and shape deduction.Furthermore,this ap-proach has implemented both explicit shape checking and implicit shape checking,to ease the application of shape checking.With this work,the extended shape system can process more powerful and more complex assertions for describing shape graphs.The function invocation calculation can also be supported in the shape system.And mutable data structures which do not conform to system definitions can be identified easily.In summary,this work has im-proved the shape system in both functionality and performance.