Skip to content

Commit bc8f9d3

Browse files
andorpandorp
committed
Run Souffle HPT
1 parent 9887597 commit bc8f9d3

File tree

8 files changed

+650
-65
lines changed

8 files changed

+650
-65
lines changed

‎datalog/hpt/hpt.dl

Lines changed: 340 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,340 @@
1+
.type Function
2+
.type Variable
3+
.type Tag
4+
.type Literal
5+
.type SimpleType
6+
.type CodeName = Variable | Function
7+
8+
// External function (name, effectful)
9+
.decl External(f:Function,effectful:number,ret:SimpleType)
10+
.decl ExternalParam(f:Function, i:number, st:SimpleType)
11+
12+
// variable
13+
// example: result <- pure value
14+
.decl Move(result:Variable, value:Variable)
15+
16+
// literal value
17+
// example: result <- pure 1
18+
.decl LitAssign(result:Variable, st:SimpleType, l:Literal)
19+
20+
// node value
21+
// example: result_node <- pure (Ctag item0 item1)
22+
.decl Node(result_node:Variable, t:Tag)
23+
.decl NodeArgument(result_node:Variable, i:number, item:Variable)
24+
25+
// store/fetch/update
26+
// example: result <- fetch value
27+
.decl Fetch(result:Variable, value:Variable)
28+
// example: result <- store value
29+
.decl Store(result:Variable, value:Variable)
30+
// example: result <- update target value
31+
.decl Update(result:Variable, target:Variable, value:Variable)
32+
33+
34+
// app a.k.a. call
35+
// example: call_result <- f value0 value1
36+
.decl Call(call_result:Variable, f:Function)
37+
.decl CallArgument(call_result:Variable, i:number, value:Variable)
38+
39+
// bind pattern
40+
// example: node@(Ctag param0 param1) <- pure input_value
41+
.decl NodePattern(node:Variable, t:Tag, input_value:Variable)
42+
.decl NodeParameter(node:Variable, i:number, parameter:Variable)
43+
44+
// function
45+
// example: f param0 param1 = ...
46+
.decl FunctionParameter(f:Function, i:number, parameter:Variable)
47+
48+
// case + alt
49+
// example:
50+
// case_result <- case scrut of
51+
// alt_value@(Ctag param0 param1) -> basic_block_name arg0 arg1
52+
.decl Case(case_result:Variable, scrutinee:Variable)
53+
.decl Alt(case_result:Variable, alt_value:Variable, t:Tag)
54+
.decl AltParameter(case_result:Variable, t:Tag, i:number, parameter:Variable)
55+
.decl AltLiteral(case_result:Variable, alt_value:Variable, st:SimpleType, l:Literal)
56+
.decl AltDefault(case_result:Variable, alt_value:Variable)
57+
58+
// pure a.k.a. return value
59+
// example: pure value
60+
.decl ReturnValue(n:CodeName, value:Variable)
61+
62+
// instruction ordering
63+
.decl FirstInst(n:CodeName, result:Variable)
64+
.decl NextInst(prev:Variable, next:Variable)
65+
66+
.decl EntryPoint(n:CodeName)
67+
68+
.input External
69+
.input ExternalParam
70+
.input Move
71+
.input LitAssign
72+
.input Node
73+
.input NodeArgument
74+
.input Fetch
75+
.input Store
76+
.input Update
77+
.input Call
78+
.input CallArgument
79+
.input NodePattern
80+
.input NodeParameter
81+
.input FunctionParameter
82+
.input Case
83+
.input Alt
84+
.input AltParameter
85+
.input AltLiteral
86+
.input AltDefault
87+
.input ReturnValue
88+
.input FirstInst
89+
.input NextInst
90+
.input EntryPoint
91+
92+
// Reachability
93+
.decl ReachableCode(n:CodeName)
94+
.output ReachableCode(delimiter=",")
95+
.decl CodeNameInst(n:CodeName, v:Variable)
96+
.output CodeNameInst(delimiter=",")
97+
98+
CodeNameInst(n, v) :-
99+
FirstInst(n, v).
100+
CodeNameInst(n, v) :-
101+
CodeNameInst(n, v0),
102+
NextInst(v0, v).
103+
104+
ReachableCode(n) :-
105+
EntryPoint(n).
106+
ReachableCode(n) :-
107+
ReachableCode(n0),
108+
CodeNameInst(n0, v),
109+
Call(v, n).
110+
111+
.decl ReachableInst(v:Variable)
112+
113+
ReachableInst(v) :-
114+
ReachableCode(n),
115+
CodeNameInst(n, v).
116+
117+
.decl VarPointsTo(v:Variable, target:Variable)
118+
.output VarPointsTo(delimiter=",")
119+
120+
VarPointsTo(v,t) :-
121+
Store(v, t),
122+
ReachableInst(v).
123+
124+
VarPointsTo(v,t) :-
125+
Move(v, v0),
126+
ReachableInst(v),
127+
VarPointsTo(v0, t).
128+
129+
VarPointsTo(v,t) :-
130+
Update(r, v, t),
131+
ReachableInst(r).
132+
133+
VarPointsTo(v,t) :-
134+
FunctionParameter(_, i, v),
135+
CallArgument(r, i, v0),
136+
VarPointsTo(v0, t),
137+
ReachableInst(r).
138+
139+
// Value Computation
140+
.decl Value(v:Variable, value:Variable)
141+
.output Value(delimiter=",")
142+
143+
.decl Heap(orig:Variable, item:Variable)
144+
.output Heap(delimiter=",")
145+
146+
Heap(v,i) :- Store(v,i).
147+
148+
// HPT: update
149+
Heap(heap_orig, sv) :-
150+
Update(_, heap, sv),
151+
Value(heap, heap_orig),
152+
Heap(heap_orig, _),
153+
SharedLocation(heap).
154+
155+
Value(n,n) :-
156+
LitAssign(n,_,_).
157+
158+
Value(n, n) :-
159+
Node(n, _).
160+
161+
Value(v, v) :-
162+
Store(v, _).
163+
164+
Value(v,v) :-
165+
Update(v,_,_).
166+
167+
Value(v,v) :-
168+
External(f,_,_),
169+
Call(v,f).
170+
171+
Value(v, n) :-
172+
Node(n, _),
173+
Move(v, n).
174+
175+
Value(v1,v2) :-
176+
FunctionParameter(_,_,p),
177+
Value(v1,p),
178+
Value(p,v2).
179+
180+
// HPT: fetch
181+
Value(v, item_origin) :-
182+
Fetch(v, heap),
183+
Value(heap, heap_orig),
184+
Heap(heap_orig, item),
185+
Value(item, item_origin).
186+
187+
// fun param
188+
Value(p, val) :-
189+
CallArgument(r, i, a),
190+
Call(r, f),
191+
FunctionParameter(f, i, p),
192+
Value(a, val).
193+
194+
// fun return
195+
Value(r, val) :-
196+
Call(r, f),
197+
ReturnValue(f, v),
198+
Value(v, val).
199+
200+
// Node parameter matching node value created somewhere
201+
Value(param, argval) :-
202+
NodePattern(v, tag, n),
203+
NodeParameter(v, i, param),
204+
Value(n, nval),
205+
Node(nval, tag),
206+
NodeArgument(nval, i, arg),
207+
Value(arg, argval).
208+
209+
// Alt value when matched on tag.
210+
Value(alt_val, scrut_val) :-
211+
Case(case_result, scrut),
212+
AltLiteral(case_result, alt_val, _, _),
213+
Value(scrut, scrut_val).
214+
215+
// Alt value when matched on tag
216+
Value(alt_val, scrut_val) :-
217+
Case(case_result, scrut),
218+
Alt(case_result, alt_val, tag),
219+
Value(scrut, scrut_val),
220+
Node(scrut_val, tag).
221+
222+
// Value of alt parameter when matched on tag
223+
Value(parameter, val) :-
224+
Case(case_res, scrut),
225+
Alt(case_res, _alt_value, tag),
226+
AltParameter(case_res, tag, i, parameter),
227+
Value(scrut, scrut_val),
228+
Node(scrut_val,tag),
229+
NodeArgument(scrut_val,i,val).
230+
231+
// Result of case/alt when matched on a node.
232+
Value(case_result, val) :-
233+
Case(case_result, _),
234+
Alt(case_result, alt_value, _),
235+
ReturnValue(alt_value, v),
236+
Value(v, val).
237+
238+
// Result of case/alt when matched on a literal.
239+
Value(case_result, val) :-
240+
Case(case_result, _),
241+
AltLiteral(case_result, alt_value, _, _),
242+
ReturnValue(alt_value, v),
243+
Value(v, val).
244+
245+
// Result of case/alt when matched on the default alternative.
246+
Value(case_result, val) :-
247+
Case(case_result, _),
248+
AltDefault(case_result, alt_value),
249+
ReturnValue(alt_value, v),
250+
Value(v, val).
251+
252+
// Type Env
253+
254+
.type NodeParamType = Variable | SimpleType
255+
.decl AbstractLocation(n: Variable)
256+
.decl VariableSimpleType(n: Variable, st:SimpleType)
257+
.decl VariableAbstractLocation(n:Variable, loc:Variable)
258+
.decl VariableNodeTag(n:Variable, t:Tag)
259+
.decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType)
260+
261+
.output AbstractLocation(delimiter=",")
262+
AbstractLocation(n) :- Heap(n,_).
263+
264+
.output VariableSimpleType(delimiter=",")
265+
VariableSimpleType(n,st) :- LitAssign(n,st,_).
266+
VariableSimpleType(n,"Unit") :- Update(n,_,_).
267+
VariableSimpleType(n,st) :- External(f,_,st), Call(n,f).
268+
VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n).
269+
VariableSimpleType(n,st) :- Value(n,r), VariableSimpleType(r,st).
270+
271+
.output VariableNodeParamType(delimiter=",")
272+
VariableNodeParamType(n,t,i,al)
273+
:- Node(n,t), NodeArgument(n,i,arg), Value(arg,al), AbstractLocation(al).
274+
VariableNodeParamType(n,t,i,st)
275+
:- Node(n,t), NodeArgument(n,i,arg), Value(arg,v), VariableSimpleType(v,st).
276+
VariableNodeParamType(n,t,i,ty)
277+
:- Value(n,n0), VariableNodeParamType(n0,t,i,ty).
278+
279+
.output VariableNodeTag(delimiter=",")
280+
VariableNodeTag(n,t) :- Value(n,r), Node(r,t).
281+
282+
.output VariableAbstractLocation(delimiter=",")
283+
VariableAbstractLocation(n,n) :- AbstractLocation(n).
284+
VariableAbstractLocation(n,v) :- Value(n,v), AbstractLocation(v).
285+
286+
.decl FunName(f: Function)
287+
.output FunName(delimiter=",")
288+
289+
.decl FunReturn(f:Function, n:Variable)
290+
.output FunReturn(delimiter=",")
291+
292+
.decl FunParam(f:Function, i:number, n:Variable)
293+
.output FunParam(delimiter=",")
294+
295+
FunName("main").
296+
FunName(f) :- Call(_,f), ReachableCode(f).
297+
298+
FunReturn(f,n) :- FunName(f), ReturnValue(f,n).
299+
FunReturn(f,n) :- External(f,_,_), Call(n,f).
300+
301+
FunParam(f,i,p) :- FunctionParameter(f,i,p).
302+
FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p).
303+
304+
/* If a concrete instance of the abstract location may be subject to a fetch more than once, */
305+
.decl SharedLocation(n:Variable)
306+
.output SharedLocation(delimiter=",")
307+
308+
SharedLocation(l) :-
309+
AbstractLocation(l), Value(v,l), NonLinearVar(v).
310+
311+
// For non-linear variables
312+
// A location may only become shared if it is a possible value of a nonlinear variable.
313+
//
314+
315+
.decl AfterInst(b:Variable,a:Variable)
316+
.output AfterInst(delimiter=",")
317+
318+
AfterInst(b,a) :- NextInst(b,a).
319+
AfterInst(b,c) :- AfterInst(b,a), NextInst(a,c).
320+
321+
.decl NonLinearVar(v:Variable)
322+
.output NonLinearVar(delimiter=",")
323+
324+
// Variable used in different use cases.
325+
// CA F M NP RV
326+
// CallArgument CA -- - x xx xx
327+
// Move M -- - - xx xx
328+
// NodeParameter NP -- - - -- xx
329+
// ReturnValue RV -- - - -- --
330+
331+
NonLinearVar(n) :- CallArgument(f,_,n), CallArgument(g,_,n), !(f=g).
332+
NonLinearVar(n) :- CallArgument(_,i,n), CallArgument(_,j,n), !(i=j).
333+
NonLinearVar(n) :- CallArgument(_,_,n), Move(_,n).
334+
NonLinearVar(n) :- CallArgument(_,_,n), NodeArgument(_,_,n).
335+
NonLinearVar(n) :- CallArgument(_,_,n), ReturnValue(_,n).
336+
NonLinearVar(n) :- Fetch(r,n), Fetch(q,n), !(r=q).
337+
NonLinearVar(n) :- Update(_,v0,n), Fetch(_,v1), AfterInst(v0,v1).
338+
NonLinearVar(n) :- Move(_,n), NodeArgument(_,_,n).
339+
NonLinearVar(n) :- Move(_,n), ReturnValue(_,n).
340+
NonLinearVar(n) :- NodeParameter(_,_,n), ReturnValue(_,n).

‎grin/app/CLI/Lib.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,7 @@ pipelineOpts =
134134
<|> (T <$> transformOpts)
135135
<|> flg ConfluenceTest "confluence-test" "Checks transformation confluence by generating random two pipelines which reaches the fix points."
136136
<|> flg PrintErrors "print-errors" "Prints the error log"
137+
<|> flg DatalogHPT "datalog-hpt" "Run HPT in souffle"
137138

138139

139140
maybeRenderingOpt :: String -> Maybe RenderingOption

‎grin/grin.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -151,6 +151,7 @@ library
151151
Transformations.ExtendedSyntax.Optimising.CSE
152152
Transformations.ExtendedSyntax.Optimising.EvaluatedCaseElimination
153153
Transformations.ExtendedSyntax.Optimising.TrivialCaseElimination
154+
Transformations.ExtendedSyntax.Normalisation
154155

155156
Transformations.BindNormalisation
156157
Transformations.CountVariableUse

0 commit comments

Comments
 (0)