Skip to content

Commit d5ece2c

Browse files
author
Jules
committed
Laurel: test the modifies frame
Structural #guards that the enumerated frame is quantifier-free while the pointwise frame is not (ModifiesFrameQuantifierFreeTest), the array-theory path including allocating bodies (T2c), and a perf/completeness regression for a chained spec procedure (T2e).
1 parent 49f5081 commit d5ece2c

3 files changed

Lines changed: 267 additions & 0 deletions

File tree

‎StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
/-
2+
Copyright Strata Contributors
3+
4+
SPDX-License-Identifier: Apache-2.0 OR MIT
5+
-/
6+
7+
/-
8+
Under `--use-array-theory`, the `ModifiesClauses` pass emits a quantifier-free
9+
heap-equation frame —
10+
`data!($heap) == update(data!(old), ref, select(data!($heap), ref))`
11+
— instead of the `forall obj fld. notModified(obj) ==> readField(old) == readField(new)`
12+
form. The same procedures must verify under either encoding; this pins the
13+
array-theory path. Mirrors `T2_ModifiesClauses` but with `useArrayTheory := true`.
14+
-/
15+
16+
import StrataTest.Util.TestLaurel
17+
18+
open StrataTest.Util
19+
open Strata
20+
21+
#eval testLaurel
22+
(options := { defaultLaurelTestOptions with
23+
translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true },
24+
verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <|
25+
#strata
26+
program Laurel;
27+
composite Container {
28+
var value: int
29+
}
30+
31+
procedure modifyContainerOpaque(c: Container) returns (b: bool)
32+
opaque
33+
modifies c
34+
{
35+
c#value := c#value + 1;
36+
true
37+
};
38+
39+
procedure caller()
40+
opaque
41+
{
42+
var c: Container := new Container;
43+
var d: Container := new Container;
44+
var x: int := d#value;
45+
var b: bool := modifyContainerOpaque(c);
46+
assert x == d#value // pass: d#value is preserved (d ∉ modifies)
47+
};
48+
49+
procedure multipleModifiesClauses(c: Container, d: Container, e: Container)
50+
opaque
51+
modifies c
52+
modifies d
53+
;
54+
55+
procedure multipleModifiesClausesCaller()
56+
opaque
57+
{
58+
var c: Container := new Container;
59+
var d: Container := new Container;
60+
var e: Container := new Container;
61+
var x: int := e#value;
62+
multipleModifiesClauses(c, d, e);
63+
assert x == e#value // pass: e is preserved (not in the modifies set)
64+
};
65+
66+
procedure newObjectDoNotCountForModifies()
67+
opaque
68+
{
69+
var c: Container := new Container;
70+
c#value := 1
71+
};
72+
73+
// Regression: an allocating body verifies under array theory (bodies use the pointwise frame).
74+
procedure allocatesInModifiesBody(c: Container) returns (b: bool)
75+
opaque
76+
modifies c
77+
{
78+
c#value := c#value + 1;
79+
var t: Container := new Container;
80+
t#value := 99;
81+
true
82+
};
83+
84+
// Regression: a body that allocates via a CALL still verifies (the callee
85+
// newObjectDoNotCountForModifies grows the heap); the pointwise frame tolerates it.
86+
procedure allocatesViaCall(c: Container) returns (b: bool)
87+
opaque
88+
modifies c
89+
{
90+
c#value := c#value + 1;
91+
newObjectDoNotCountForModifies();
92+
true
93+
};
94+
95+
// Soundness: writes outside the modifies clause are still rejected.
96+
97+
procedure modifyContainerWithoutPermission2(c: Container, d: Container)
98+
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
99+
opaque
100+
modifies d
101+
{
102+
c#value := 2
103+
};
104+
105+
procedure modifyContainerWithoutPermission3(c: Container, d: Container)
106+
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
107+
opaque
108+
modifies d
109+
{
110+
var i: bool := modifyContainerOpaque(c)
111+
};
112+
#end

‎StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
/-
2+
Copyright Strata Contributors
3+
4+
SPDX-License-Identifier: Apache-2.0 OR MIT
5+
-/
6+
7+
/-
8+
Perf / regression: the array-theory frame is not merely faster, it is more
9+
complete on heap-heavy code.
10+
11+
`stress` makes a deep chain of opaque heap-modifying calls on freshly allocated
12+
objects, then asserts that an object allocated *before* the chain is untouched.
13+
14+
- Under the `∀` frame (array theory off) the solver cannot instantiate the
15+
quantified frame across the whole chain: the assertion "could not be proved".
16+
This is a definite verdict in ~2s, not a wall-clock timeout.
17+
- Under the quantifier-free frame (`--use-array-theory`) the same assertion
18+
verifies: each step is a `store` on a single row, so the read of the
19+
untouched object is a pure array rewrite with nothing to instantiate.
20+
21+
The two blocks are identical apart from `useArrayTheory`.
22+
23+
Note: the `∀` outcome depends on the SMT solver's quantifier heuristics. If a
24+
future solver discharges it, the annotation below must be updated.
25+
-/
26+
27+
import StrataTest.Util.TestLaurel
28+
29+
open StrataTest.Util
30+
open Strata
31+
32+
-- ∀ frame (array theory off): the chain defeats quantifier instantiation.
33+
#eval testLaurel
34+
(options := { defaultLaurelTestOptions with
35+
translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := false },
36+
verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := false } }) <|
37+
#strata
38+
program Laurel;
39+
composite Container {
40+
var value: int
41+
}
42+
43+
procedure modifyOne(c: Container)
44+
opaque
45+
modifies c;
46+
47+
procedure stress()
48+
opaque
49+
modifies *
50+
{
51+
var target: Container := new Container;
52+
var x: int := target#value;
53+
var c0: Container := new Container; modifyOne(c0);
54+
var c1: Container := new Container; modifyOne(c1);
55+
var c2: Container := new Container; modifyOne(c2);
56+
var c3: Container := new Container; modifyOne(c3);
57+
var c4: Container := new Container; modifyOne(c4);
58+
var c5: Container := new Container; modifyOne(c5);
59+
var c6: Container := new Container; modifyOne(c6);
60+
var c7: Container := new Container; modifyOne(c7);
61+
var c8: Container := new Container; modifyOne(c8);
62+
var c9: Container := new Container; modifyOne(c9);
63+
var c10: Container := new Container; modifyOne(c10);
64+
var c11: Container := new Container; modifyOne(c11);
65+
var c12: Container := new Container; modifyOne(c12);
66+
var c13: Container := new Container; modifyOne(c13);
67+
var c14: Container := new Container; modifyOne(c14);
68+
var c15: Container := new Container; modifyOne(c15);
69+
var c16: Container := new Container; modifyOne(c16);
70+
var c17: Container := new Container; modifyOne(c17);
71+
var c18: Container := new Container; modifyOne(c18);
72+
var c19: Container := new Container; modifyOne(c19);
73+
assert x == target#value
74+
//^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
75+
};
76+
#end
77+
78+
-- Quantifier-free frame (--use-array-theory): the same program verifies.
79+
#eval testLaurel
80+
(options := { defaultLaurelTestOptions with
81+
translateOptions := { defaultLaurelTestOptions.translateOptions with useArrayTheory := true },
82+
verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <|
83+
#strata
84+
program Laurel;
85+
composite Container {
86+
var value: int
87+
}
88+
89+
procedure modifyOne(c: Container)
90+
opaque
91+
modifies c;
92+
93+
procedure stress()
94+
opaque
95+
modifies *
96+
{
97+
var target: Container := new Container;
98+
var x: int := target#value;
99+
var c0: Container := new Container; modifyOne(c0);
100+
var c1: Container := new Container; modifyOne(c1);
101+
var c2: Container := new Container; modifyOne(c2);
102+
var c3: Container := new Container; modifyOne(c3);
103+
var c4: Container := new Container; modifyOne(c4);
104+
var c5: Container := new Container; modifyOne(c5);
105+
var c6: Container := new Container; modifyOne(c6);
106+
var c7: Container := new Container; modifyOne(c7);
107+
var c8: Container := new Container; modifyOne(c8);
108+
var c9: Container := new Container; modifyOne(c9);
109+
var c10: Container := new Container; modifyOne(c10);
110+
var c11: Container := new Container; modifyOne(c11);
111+
var c12: Container := new Container; modifyOne(c12);
112+
var c13: Container := new Container; modifyOne(c13);
113+
var c14: Container := new Container; modifyOne(c14);
114+
var c15: Container := new Container; modifyOne(c15);
115+
var c16: Container := new Container; modifyOne(c16);
116+
var c17: Container := new Container; modifyOne(c17);
117+
var c18: Container := new Container; modifyOne(c18);
118+
var c19: Container := new Container; modifyOne(c19);
119+
assert x == target#value
120+
};
121+
#end

‎StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
/-
2+
Copyright Strata Contributors
3+
4+
SPDX-License-Identifier: Apache-2.0 OR MIT
5+
-/
6+
7+
/-
8+
Structural check, independent of the solver: the enumerated modifies frame
9+
(`buildEnumeratedFrame`) must contain no quantifier, so there is nothing for the
10+
solver to instantiate. The `∀`-based frame it replaces (`buildPointwiseFrame`)
11+
does contain one; asserting both pins the property and shows the check
12+
discriminates between the two encodings.
13+
-/
14+
15+
import Strata.Languages.Laurel.ModifiesClauses
16+
17+
open Strata.Laurel
18+
19+
namespace StrataTest.Laurel.ModifiesFrameQuantifierFree
20+
21+
private def selfRef : StmtExprMd := { val := .Var (.Local "self"), source := none }
22+
private def heapIn : StmtExprMd := { val := .Var (.Local "$heap_in"), source := none }
23+
private def heapOut : StmtExprMd := { val := .Var (.Local "$heap"), source := none }
24+
private def singleRefModifies : List ModifiesEntry := [.single selfRef]
25+
26+
/-- Whether the (pretty-printed) frame mentions a quantifier. -/
27+
private def hasQuantifier (e : StmtExprMd) : Bool :=
28+
let s := reprStr e
29+
(s.splitOn "forall").length > 1 || (s.splitOn "exists").length > 1
30+
31+
#guard !hasQuantifier (buildEnumeratedFrame default singleRefModifies heapIn heapOut)
32+
#guard hasQuantifier (buildPointwiseFrame default singleRefModifies heapIn heapOut)
33+
34+
end StrataTest.Laurel.ModifiesFrameQuantifierFree

0 commit comments

Comments
 (0)