1- using Amb
1+ # ### Path
2+
3+ # First just do it for the case where there we assume
4+ # tainted gotoifnots do not go in a loop!
5+ # TODO : write a thing to detect this! (overdub predicates only in tainted ifs)
6+ # implement snapshotting function state as an optimization for branch exploration
7+ mutable struct Path
8+ path:: BitVector
9+ cursor:: Int
10+ end
11+
12+ Path () = Path ([], 1 )
13+
14+ function increment! (bitvec)
15+ for i= 1 : length (bitvec)
16+ if bitvec[i] === true
17+ bitvec[i] = false
18+ else
19+ bitvec[i] = true
20+ break
21+ end
22+ end
23+ end
24+
25+ function reset! (p:: Path )
26+ p. cursor= 1
27+ increment! (p. path)
28+ nothing
29+ end
30+
31+ function alldone (p:: Path ) # must be called at the end of the function!
32+ all (identity, p. path)
33+ end
34+
35+ function current_predicate! (p:: Path )
36+ if p. cursor > length (p. path)
37+ push! (p. path, false )
38+ else
39+ p. path[p. cursor]
40+ end
41+ val = p. path[p. cursor]
42+ p. cursor+= 1
43+ val
44+ end
45+
46+ alldone (c) = alldone (c. metadata[2 ])
47+ reset! (c) = reset! (c. metadata[2 ])
48+ current_predicate! (c) = current_predicate! (c. metadata[2 ])
49+
50+ #=
51+ julia> p=Path()
52+ Path(Bool[], 1)
53+
54+ julia> alldone(p) # must be called at the end of a full run
55+ true
56+
57+ julia> current_predicate!(p)
58+ false
59+
60+ julia> alldone(p) # must be called at the end of a full run
61+ false
62+
63+ julia> current_predicate!(p)
64+ false
65+
66+ julia> p
67+ Path(Bool[false, false], 3)
68+
69+ julia> alldone(p)
70+ false
71+
72+ julia> reset!(p)
73+
74+ julia> p
75+ Path(Bool[true, false], 1)
76+
77+ julia> current_predicate!(p)
78+ true
79+
80+ julia> current_predicate!(p)
81+ false
82+
83+ julia> alldone(p)
84+ false
85+
86+ julia> reset!(p)
87+
88+ julia> p
89+ Path(Bool[false, true], 1)
90+
91+ julia> current_predicate!(p)
92+ false
93+
94+ julia> current_predicate!(p)
95+ true
96+
97+ julia> reset!(p)
98+
99+ julia> current_predicate!(p)
100+ true
101+
102+ julia> current_predicate!(p)
103+ true
104+
105+ julia> alldone(p)
106+ true
107+ =#
2108
3109"""
4110`abstract_run(g, ctx, overdubbed_fn, args...)`
32138# do something to merge metadata from all the runs
33139```
34140"""
35- function abstract_run (acc, ctx:: Cassette.Context , overdub_fn, args... )
36- pass_ctx = Cassette. similarcontext (ctx, pass= AbsintPass)
37- acc (Cassette. overdub (pass_ctx, overdub_fn, args... ))
141+ function abstract_run (acc, ctx:: Cassette.Context , overdub_fn, args... ; verbose= true )
142+ path = Path ()
143+ pass_ctx = Cassette. similarcontext (ctx, metadata= (ctx. metadata, path), pass= AbsintPass)
144+
145+ while true
146+ acc (Cassette. recurse (pass_ctx, ()-> overdub_fn (args... )))
147+
148+ verbose && println (" Explored path: " , path)
149+ alldone (path) && break
150+ reset! (path)
151+ end
38152end
39153
40154"""
@@ -47,8 +161,6 @@ function istainted(ctx, cond)
47161 " See docs for `istainted`." )
48162end
49163
50- _choice () = (@amb true false )
51-
52164# Must return 7 exprs
53165function rewrite_branch (ctx, stmt, extraslot, i)
54166 # turn
@@ -70,9 +182,9 @@ function rewrite_branch(ctx, stmt, extraslot, i)
70182 # not tainted? jump to the penultimate statement
71183 push! (exprs, Expr (:gotoifnot , istainted_ssa, i+ 5 ))
72184
73- # tainted? then use this_here_predicate !(SSAValue(1))
185+ # tainted? then use current_predicate !(SSAValue(1))
74186 current_pred = i+ 2
75- push! (exprs, :($ _choice ( )))
187+ push! (exprs, :($ ( Expr ( :nooverdub , current_predicate!))( $ ( Expr ( :contextslot )) )))
76188
77189 # Store the interpreter-provided predicate in the slot
78190 push! (exprs, Expr (:(= ), extraslot, SSAValue (i+ 2 )))
@@ -93,7 +205,7 @@ function rewrite_ir(ctx, ref)
93205 # turn
94206 # <val> ? t : f
95207 # into
96- # istainted(<val>) ? this_here_predicate !(p) : <val> ? t : f
208+ # istainted(<val>) ? current_predicate !(p) : <val> ? t : f
97209
98210 ir = ref. code_info
99211 ir = copy (ir)
0 commit comments