4 A pointer logic and certifying compiler 2 The pointer logic A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.It is mainly used to eliminate context-sensitive errors in programs.A traditional type system is not enough when the legality of a phrase depends not only on the context but also on some expression values in the phrase.One solution is to use dependent types 7.Another solution is not to deem the constraints on values as parts of the type system,and the constraints don't appear in the typing rules.The former makes the type system complicated and the latter makes it an unsound type system. We try to investigate a trade-off between these two solutions in the design of PointerC.To make the type system simple and guarantee the safety of the language at the same time,side conditions are introduced into the typing rules to express the constraints on values.For example,in the following two typing rules, side conditions contain the constraints on subscript expressions and pointers TFe:int TFa:array(10,bool) 0≤e∧e<9 TFa[e]bool T-p:ptr(struct(...,x:int,...)) THp->x:int p∈effective-ptrs These side conditions must be checked.And to check these side conditions statically,we have designed a pointer logic for PointerC.The design of the pointer logic is inspired by the following facts and speculations: 1.At a program point,if we know whether a pointer is an effective pointer (a pointer which points to an object),a null pointer or a dangling pointer and the equality relation between all the effective pointers,we can deduce whether a pointer operation is safe or not.And we can also capture the change of the pointer information after this operation. 2.A logic system may not able to prove the safety of all programs.But it is still feasible if it can prove the safety of most programs. 3.The pointer information collected by Hoare-style reasoning can be used to reason about program properties.It amounts to combining program analysis with program verification and this combination has a brilliant future. To present the pointer logic,we make clear some pointer-related terms and notations first,and then explain some elementary operations used in the pointer logic.After that,we introduce the inference rules in our pointer logic. 2.1 Conventions,terminologies and notations Dynamic variables can only be accessed through declared pointer variables.For example,s->data,s->next->pre,*s and *s [5]etc.Such expressions are called symbolic access paths of variables,access paths for short.Note that s->next is4 A pointer logic and certifying compiler 2 The pointer logic A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. It is mainly used to eliminate context-sensitive errors in programs. A traditional type system is not enough when the legality of a phrase depends not only on the context but also on some expression values in the phrase. One solution is to use dependent types [7]. Another solution is not to deem the constraints on values as parts of the type system, and the constraints don’t appear in the typing rules. The former makes the type system complicated and the latter makes it an unsound type system. We try to investigate a trade-off between these two solutions in the design of PointerC. To make the type system simple and guarantee the safety of the language at the same time, side conditions are introduced into the typing rules to express the constraints on values. For example, in the following two typing rules, side conditions contain the constraints on subscript expressions and pointers. Γ `e : int Γ `a : array(10, bool) Γ `a[e] : bool 0 ≤ e ∧ e ≤ 9 Γ `p : ptr(struct(. . . , x:int, . . . )) Γ `p->x : int p ∈ effective ptrs These side conditions must be checked. And to check these side conditions statically, we have designed a pointer logic for PointerC. The design of the pointer logic is inspired by the following facts and speculations: 1. At a program point, if we know whether a pointer is an effective pointer (a pointer which points to an object), a null pointer or a dangling pointer and the equality relation between all the effective pointers, we can deduce whether a pointer operation is safe or not. And we can also capture the change of the pointer information after this operation. 2. A logic system may not able to prove the safety of all programs. But it is still feasible if it can prove the safety of most programs. 3. The pointer information collected by Hoare-style reasoning can be used to reason about program properties. It amounts to combining program analysis with program verification and this combination has a brilliant future. To present the pointer logic, we make clear some pointer-related terms and notations first, and then explain some elementary operations used in the pointer logic. After that, we introduce the inference rules in our pointer logic. 2.1 Conventions, terminologies and notations Dynamic variables can only be accessed through declared pointer variables. For example, s->data, s->next->pre, *s and *s[5] etc. Such expressions are called symbolic access paths of variables, access paths for short. Note that s->next is