Gradual C0 Symbolic Execution for Gradual Verification_2
2025-04-29
0
0
1.95MB
50 页
10玖币
侵权投诉
Gradual C0: Symbolic Execution for Gradual Verification
JENNA DIVINCENZO, Purdue University, USA
IAN MCCORMACK, Carnegie Mellon University, USA
HEMANT GOUNI, Carnegie Mellon University, USA
JACOB GORENBURG, Haverford College, USA
JAN-PAUL RAMOS-DÁVILA, Cornell University, USA
MONA ZHANG, Columbia University, USA
CONRAD ZIMMERMAN, Brown University, USA
JOSHUA SUNSHINE, Carnegie Mellon University, USA
ÉRIC TANTER, University of Chile, Chile
JONATHAN ALDRICH, Carnegie Mellon University, USA
Current static verication techniques such as separation logic support a wide range of programs. However,
such techniques only support complete and detailed specications, which places an undue burden on users.
To solve this problem, prior work proposed gradual verication, which handles complete, partial, or missing
specications by soundly combining static and dynamic checking. Gradual verication has also been extended
to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension
does not reward users with decreased dynamic checking as specications are rened. In fact, all properties
are checked dynamically regardless of any static guarantees. Additionally, no full-edged implementation of
gradual verication exists so far, which prevents studying its performance and applicability in practice.
We present Gradual C0, the rst practicable gradual verier for recursive heap data structures, which targets
C0, a safe subset of C designed for education. Static veriers supporting separation logic or implicit dynamic
frames use symbolic execution for reasoning; so Gradual C0, which extends one such verier, adopts symbolic
execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach
addresses technical challenges related to symbolic execution with imprecise specications, heap ownership,
and branching in both program statements and specication formulas. We also deal with challenges related
to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0.
Finally, we provide the rst empirical performance evaluation of a gradual verier, and found that on average,
Gradual C0 decreases run-time overhead between 11-34% compared to the fully-dynamic approach used in
prior work. Further, the worst-case scenarios for performance are predictable and avoidable. This work paves
the way towards evaluating gradual verication at scale.
CCS Concepts: •Theory of computation
→
Logic and verication;Automated reasoning;Hoare logic;
Separation logic.
1 INTRODUCTION
Separation logic [Reynolds 2002] supports the modular static verication of heap-manipulating
programs. Its variant Implicit dynamic frames (IDF) [Smans et al
.
2009] and extension with recursive
∗
This material is based upon work supported by a Google PhD Fellowship award and the National Science Foundation under
Grant Nos. CCF-1901033, DGE1745016, and DGE2140739. É. Tanter is partially funded by the ANID FONDECYT Regular
Project 1190058 and the Millennium Science Initiative Program: code ICN17_002. Any opinions, ndings, and conclusions
or recommendations expressed in this material are those of the authors and do not necessarily reect the views of the
National Science Foundation, Google, ANID, or the Millennium Science Initiative.
Authors’ addresses: Jenna DiVincenzo, Purdue University, USA, jennad@purdue.edu; Ian McCormack, Carnegie Mellon
University, USA, icmccorm@cs.cmu.edu; Hemant Gouni, Carnegie Mellon University, USA, hsgouni@cs.cmu.edu; Jacob
Gorenburg, Haverford College, USA, jgorenburg@haverford.edu; Jan-Paul Ramos-Dávila, Cornell University, USA, jvr34@
cornell.edu; Mona Zhang, Columbia University, USA, mz2781@columbia.edu; Conrad Zimmerman, Brown University, USA,
conrad_zimmerman@brown.edu; Joshua Sunshine, Carnegie Mellon University, USA, sunshine@cs.cmu.edu; Éric Tanter,
University of Chile, Chile, etanter@dcc.uchile.cl; Jonathan Aldrich, Carnegie Mellon University, USA, jonathan.aldrich@cs.
cmu.edu.
arXiv:2210.02428v3 [cs.LO] 19 Jan 2024
1:2
J. DiVincenzo, I. McCormack, H. Gouni, J. Gorenburg, J. Ramos-Dávila, M. Zhang, C. Zimmerman, J. Sunshine, É. Tanter, J.
Aldrich
abstract predicates [Parkinson and Bierman 2005;Smans et al
.
2009] further support verifying
recursive heap data structures, such as trees, lists, and graphs. While these techniques allow users
to specify and verify more code than ever before, tools implementing them (e.g. Viper [Müller et al
.
2016], VeriFast [Jacobs et al
.
2011], Chalice [Leino et al
.
2009], JStar [Distefano and Parkinson J
2008], and SmallFoot [Berdine et al
.
2006]) are still largely unused due to the burden they place on
their users. Such tools poorly support partial specications, and thus require users to provide a
number of auxiliary specications (such as folds, unfolds, loop invariants, and inductive lemmas)
in an all or nothing fashion to support inductive proofs of correctness. The tools also require
many of these auxiliary specications to be written before they can provide feedback on the
correctness of specications for important functional properties. For example, to prove that a
simple insertion function preserves list acyclicity, static verifers need 1.5 times as many lines of
auxiliary specications to program code (§2). They also need a signicant number of these auxiliary
specications to uncover problems with specications of the acyclic property (§2).
Inspired by gradual typing [Siek and Taha 2006], Bader et al
.
[2018] proposed gradual verication
to support the incremental specication and verication of software. Users can write imprecise (i.e.
partial) specications backed by run-time checking where necessary. An imprecise formula can be
fully unknown, written
?
, or combine a static part with the unknown, as in
?∗𝑥.𝑓 ==
2.Wise et al
.
[2020] extend Bader et al
.
[2018]’s initial system by designing and formalizing the rst gradual
verier for recursive heap data structures. It supports imprecise specications with accessibility
predicates from IDF and abstract predicates; and thus, also (in theory) the run-time verication
of these constructs. During static verication, an imprecise specication can be optimistically
strengthened (in non-contradictory ways) by the verier to support proof goals. Wherever such
strengthenings occur, dynamic checks are inserted to preserve soundness. Gradual verication
smoothly supports the spectrum between static and dynamic verication. This is captured by
properties adapted from gradual typing [Siek et al
.
2015], namely the gradual guarantee, stating that
the verier will not ag static or dynamic errors for specications that are correct but imprecise,
and the fact that gradual verication conservatively extends static verication, i.e. they coincide on
fully-precise programs.
While promising, Wise et al
.
[2020]’s gradual verier has neither been implemented nor validated
in practice. Furthermore, their design relies on weakest liberal preconditions [Dijkstra 1975] for
static reasoning rather than symbolic execution [King 1976], which is the ideal reasoning technique
for tools based on separation logic or IDF. Indeed, Viper [Müller et al
.
2016], VeriFast [Jacobs et al
.
2011], JStar [Distefano and Parkinson J 2008], and SmallFoot [Berdine et al
.
2006] all support these
permission logics with symbolic execution, not weakest liberal preconditions. Finally, Wise et al
.
[2020]’s gradual verier is not ecient in the sense that it checks all memory safety and functional
properties dynamically regardless of the precision of specications.
This paper presents the design, implementation, and validation of Gradual C0
1
—the rst grad-
ual verier for imperative programs manipulating recursive heap data structures that is based
on symbolic execution. Gradual C0 targets C0, a safe subset of C designed for education, with
appropriate support (and pedagogical material) for dynamic verication. Technically, Gradual C0 is
built on top of the Viper static verication infrastructure [Müller et al
.
2016], which facilitates the
development of program veriers supporting IDF and recursive abstract predicates. Gradual C0’s
back-end leverages this infrastructure to simplify the implementation of gradual veriers for other
programming languages, and Gradual C0’s front-end demonstrates how this is done for C0. Further,
Gradual C0 minimizes the insertion of dynamic checks using statically available information and
optimizes the checks’ overhead at run time.
1Gradual C0 is hosted on Github: https://github.com/gradual-verication/gvc0.
Gradual C0 1:3
Overall, we address new technical challenges in gradual verication related to symbolic execution,
extensibility to multiple programming languages, and minimizing run-time checks and their
overhead:
•
Gradual C0’s symbolic execution algorithm is responsible for statically verifying programs
with imprecise specications and producing minimized run-time checks. In particular, Gradual
C0 tracks the branch conditions created by program statements and specications to produce
run-time checks for corresponding execution paths. At run time, branch conditions are assigned
to variables at the branch point that introduced them, which are then used to coordinate the
successive checks as required. Further, Gradual C0 creates run-time checks by translating
symbolic expressions into specications—reversing the symbolic execution process.
•
The run-time checks produced by Gradual C0 contain branch conditions, simple logical expres-
sions, accessibility predicates, separating conjunctions, and predicates. Each of these constructs
is specially translated into source code that can be executed at run time for dynamic verication.
Logical expressions are turned into assertions. Accessibility predicates and separating conjunc-
tions are checked by tracking and updating a set of owned heap locations. Finally, predicates are
translated into recursive boolean functions. By encoding run-time checks into C0 source code,
we avoid complexities from augmenting the C0 compiler to support dynamic verication. We
also design these encodings to be performance friendly, e.g. owned heap locations are tracked
in a dynamic hash table.
Work on gradual typing performance has shown that minimizing the insertion of dynamic checks
does not trivially correlate with overall execution performance; the nature of the inserted checks
(such as higher-order function wrappers) as well as their location in the overall execution ow of a
program can have drastic and hard-to-predict consequences [Campora et al
.
2018;Feltey et al
.
2018;
Takikawa et al
.
2016]. Therefore, our validation of Gradual C0 aims to empirically evaluate the
relationship between minimizing check insertion and observed run-time performance in gradual
verication. We evaluate the performance of Gradual C0 by adapting Takikawa et al
.
[2016]’s
performance lattice method to gradual verication, exploring the performance characteristics for
partial specications of four common data structures. This method models the gradual verication
process as a series of steps of partial specications from an unspecied program (containing all
?
s)
to a statically veriable specication (not containing any
?
s) where, at each step, an atomic conjunct
is added to the current, partial specication. Statically, we observe that as more specications are
added, more verication conditions can be statically discharged. Though imprecision introduces
unavoidable run-time checks, gradual verication decreases run-time overhead by an average
of 11-34% compared to dynamic verication (and thus Wise et al
.
[2020]’s approach). Sources
of run-time overhead correspond to the predictions made in prior work, and our study shows
that the gradual guarantee holds empirically for our tool across thousands of sampled imprecise
specications.
2GRADUAL C0 IMPROVES THE STATIC SPECIFICATION PROCESS
Static verication tools, like Viper [Müller et al
.
2016], VeriFast [Jacobs et al
.
2011], Chalice [Leino
et al
.
2009], JStar [Distefano and Parkinson J 2008], and SmallFoot [Berdine et al
.
2006], require a
number of user-provided auxiliary specications, such as folds, unfolds, lemmas, and loop invariants,
to prove properties about recursive heap data structures. Worse, they also require users to write
many of these auxiliary specications before the tools can provide useful feedback on the correctness
of other specications, including ones containing important functional properties. Therefore, users
are burdened by writing many detailed and extraneous specications with inadequate static feedback
through the process. In this section, we illustrate this burden with a simple list insertion example
1:4
J. DiVincenzo, I. McCormack, H. Gouni, J. Gorenburg, J. Ramos-Dávila, M. Zhang, C. Zimmerman, J. Sunshine, É. Tanter, J.
Aldrich
(inspired by a similar introductory example and discussion from Wise et al
.
[2020]) and output from
Viper. Then, we show in §3how Gradual C0 overcomes this burden by smoothly supporting the
spectrum between static and dynamic checking. Users can avoid writing auxiliary specications
and still get sound verication of their code with increased run-time checking. Users can also
receive run-time feedback on the correctness of their specications very early in the specication
process, and the resulting error messages closely align with inherent problems in the specications
or in the program, making debugging them easier.
1str uct Node { int v al ; st ru ct Node * ne xt ; };
2ty pe de f s tr uc t No de N od e ;
3
4Node * i nse rt La st ( N ode * list , int va l )
5{
6Node * y = li st ;
7while (y - > n e xt != NULL)
8{ y = y- > next ; }
9y - > ne xt = alloc( st ru ct Node );
10 y - >nex t - > val = va l ;
11 y - > next - > next = NULL;
12 return list;
13 }
Fig. 1. Non-empty linked list insertion in C0
Fig. 1implements a linked list and function
that inserts a new node at the end of a given
list, called
insertLast
, in C0 [Arnold 2010]. The
insertLast
function traverses the list to its end
with a
while
loop starting from the root. That
is,
insertLast
implicitly assumes the list is non-
empty (non-null) and acyclic; and that for mul-
tiple successive calls to
insertLast
the list re-
mains acyclic and non-empty after insertion.
These facts can be proven explicitly with static
verication; the complete static specication is
given in Fig. 2, highlighted in grey.
List acyclicity is specied with two predicates
acyclicSeg and acyclic:
predicate acyclicSeg(Node* s, Node* e) =
s == e ? true : acc(s->val)&& acc(s->next)&& acyclicSeg(s->next, e)
predicate acyclic(Node* n) = acyclicSeg(Node* n, NULL)
The
acyclicSeg
predicate uses accessibility predicates and the separating conjunction from IDF.
Ownership is ensured through accessibility predicates such as
acc(s->val)
; and,
acc(s->val)
&&
s->val ==
2states that
s->val
is uniquely owned and contains the value 2. The separating conjunc-
tion, denoted by &&,
2
ensures memory disjointness:
acc(s->next)
&&
acc(s->next->next)
states
that the heap locations
s->next
and
s->next->next
are distinct (i.e.
𝑠≠s->next
) and are each
owned.
Thus, the abstract recursive predicate
acyclicSeg
, which can be thought of as a pure boolean
function, species that a list segment is acyclic. That is,
acyclicSeg(s, e)
denotes that all heap
locations in list
s
are distinct up to node
e
by recursively generating accessibility predicates for each
node in
s
up to
e
, joined with the separating conjunction. Further,
acyclicSeg(n, NULL)
denotes
that all heap locations in list nare distinct and so nis acyclic, as specied with acyclic(n).
Now that we have specied
acyclic
, we use it in
insertLast
’s precondition (line 5) and postcon-
dition (lines 6-7) to denote preservation of list acyclicity. We also specify that
insertLast
preserves
list non-nullness with simple comparison logic (i.e.
list != NULL
and
\result != NULL
). Ideally, we
would stop here and static veriers would be able to prove
insertLast
’s implementation is correct
with respect to this specication; however, as you can see in Fig. 2such tools require many more
specications. In fact, there are 27 lines of auxiliary specications (comprised of folds, unfolds, loop
invariants, and inductive lemmas); in contrast to 18 lines of wanted specications (the predicates
and pre- and postconditions) and program code. Furthermore, these auxiliary specications are
complex, as discussed next.
2Most IDF papers use ∗to denote the separating conjuction. We follow Viper and use && instead.
Gradual C0 1:5
1/*@ predicate acyclicSeg(Node* s, Node* e) =
2(s == e) ? true : acc(s->val) && acc(s->next) && acyclicSeg(s->next,e); @*/
3//@ predicate acyclic(Node* n) = acyclicSeg(n, NULL);
4Node * i nse rt La st ( N ode * list , int va l )
5// @ requires acyclic(list) && list != NULL ;
6/* @ e ns u re s acyclic(\result) &&
7\result != NULL ; @ */
8{
9//@ unfold acyclic(list);
10 //@ unfold acyclicSeg(list, NULL);
11 Node * y = li st ;
12 //@ fold acyclicSeg(list, y);
13 while ( y -> n ex t != NULL)
14 /* @ loop_invariant acyclicSeg(list, y) &&
15 acc(y->next) && acc(y->val) &&
16 acyclicSeg(y->next, NULL) ; @ * /
17 {
18 Node * tm p = y;
19 y = y - > ne xt ;
20 //@ unfold acyclicSeg(y, NULL);
21 //@ fold acyclicSeg(tmp->next, y);
22 //@ fold acyclicSeg(tmp, y);
23 mergeLemma(list, tmp, y);
24 }
25
26
27 y - > ne xt = alloc( st ru ct No de );
28 y - >nex t - > val = va l ;
29 y - > next - > next = NULL;
30 //@ fold acyclicSeg(y->next->next, NULL);
31 //@ fold acyclicSeg(y->next, NULL);
32 //@ fold acyclicSeg(y, NULL);
33 mergeLemma(list, y, NULL);
34 //@ fold acyclic(list);
35 return list;
36 }
37
38 void mergeLemma (Node* a, Node* b, Node* c)
39 //@ requires acyclicSeg(a, b) && acyclicSeg(b, c);
40 //@ ensures acyclicSeg(a, c);
41 {
42 if (a == b) {
43 } else {
44 //@ unfold acyclicSeg(a, b);
45 mergeLemma(a->next, b, c);
46 //@ fold acyclicSeg(a, c);
47 }
48 }
□Program code ■Static specication
Fig. 2. The static verification of insertLast from Fig. 1
2.1 Auxiliary Specifications
Static veriers cannot reliably unroll recursive predicates during verication; so, such tools rely
on explicit fold and unfold statements to control the availability of predicate information in the
verier. This treats predicates iso-recursively; while an equi-recursive interpretation treats predicates
as their complete unrolling [Summers and Drossopoulou 2013]. Consequently, the
acyclic
and
acyclicSeg
predicates are unfolded and folded often in Fig. 2(lines 9-10,12,20-22,30-32, and
34). Looking closely, we see that
acyclic(list)
, which is assumed true from the precondition, is
unfolded on line 9. This consumes
acyclic(list)
and produces its body
acyclicSeg(list, NULL)
,
which is subsequently unfolded on line 10. Then, at the fold on line 34, the body of
acyclic(list)
is packed up into the predicate itself to prove the list remains acyclic after insertion.
Additionally, static veriers cannot tell if or when a loop will end (in our example the verier
cannot tell when the list being iterated over ends), but must verify all paths through the program.
Therefore, static veriers reason about loops using specications called loop invariants, which are
properties that are preserved for each execution of the loop including at entry and exit. Further,
loop invariants must also provide information necessary for proof obligations after the loop, e.g.
that the list in
insertLast
is acyclic after insertion. In Fig. 2, these constraints result in the loop
invariant on lines 14-16 that segments the list into three disjoint and acyclic parts: from the root up
to the current node
y
(
acyclicSeg(list, y)
), the current node
y
(
acc(y->val)
&&
acc(y->next)
),
and from the node after
y
to the end (
acyclicSeg(y->next, NULL)
). Exposing
y
via its accessibility
predicates provides access to
y->next
on line 19 in the loop body; and,
acyclicSeg(list, y)
helps
prove acyclic(list) holds after the loop, as we will see next.
摘要：
展开>>
收起<<
GradualC0:SymbolicExecutionforGradualVerificationJENNADIVINCENZO,PurdueUniversity,USAIANMCCORMACK,CarnegieMellonUniversity,USAHEMANTGOUNI,CarnegieMellonUniversity,USAJACOBGORENBURG,HaverfordCollege,USAJAN-PAULRAMOS-DÁVILA,CornellUniversity,USAMONAZHANG,ColumbiaUniversity,USACONRADZIMMERMAN,BrownUniv...
声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！
分类：图书资源
价格：10玖币
属性：50 页
大小：1.95MB
格式：PDF
时间：2025-04-29
作者详情
-
Optimal Persistent Monitoring of Mobile Targets in One Dimension Jonas Hall1 Sean Andersson12 Christos G. Cassandras13 Abstract This work shows the existence of opti-10 玖币0人下载
-
Optimal metabolic strategies for microbial growth in stationary random environments Anna Paola Muntoni and Andrea De Martino10 玖币0人下载
相关内容
-
行政事业单位内部控制报告-关于印发编外聘用人员管理制度和编外聘用人员年度考核制度
分类：办公文档
时间：2025-03-03
标签：无
格式：DOC
价格：5.9 玖币
-
行政事业单位内部控制报告-风险评估管理制度
分类：办公文档
时间：2025-03-03
标签：无
格式：DOCX
价格：5.9 玖币
-
行政事业单位内部控制报告-采购管理内部控制制度
分类：办公文档
时间：2025-03-03
标签：无
格式：DOCX
价格：5.9 玖币
-
行政事业单位内部控制报告-部署单位内部控制专题培训和风险评估工作会议纪要
分类：办公文档
时间：2025-03-03
标签：无
格式：DOC
价格：5.9 玖币
-
行政事业单位内部控制报告-关键岗位轮岗及专项审计制度
分类：办公文档
时间：2025-03-03
标签：关键
格式：DOCX
价格：5.9 玖币
渝公网安备50010702506394
