Skip to content

Commit 7f12b5e

Browse files
committed
Datalog: Create HPTResult from souffle output.
1 parent bc8f9d3 commit 7f12b5e

File tree

3 files changed

+244
-25
lines changed

3 files changed

+244
-25
lines changed

datalog/hpt/hpt.dl

+16-16
Original file line numberDiff line numberDiff line change
@@ -91,9 +91,9 @@
9191

9292
// Reachability
9393
.decl ReachableCode(n:CodeName)
94-
.output ReachableCode(delimiter=",")
94+
// .output ReachableCode
9595
.decl CodeNameInst(n:CodeName, v:Variable)
96-
.output CodeNameInst(delimiter=",")
96+
// .output CodeNameInst
9797

9898
CodeNameInst(n, v) :-
9999
FirstInst(n, v).
@@ -115,7 +115,7 @@ ReachableInst(v) :-
115115
CodeNameInst(n, v).
116116

117117
.decl VarPointsTo(v:Variable, target:Variable)
118-
.output VarPointsTo(delimiter=",")
118+
.output VarPointsTo
119119

120120
VarPointsTo(v,t) :-
121121
Store(v, t),
@@ -138,10 +138,10 @@ VarPointsTo(v,t) :-
138138

139139
// Value Computation
140140
.decl Value(v:Variable, value:Variable)
141-
.output Value(delimiter=",")
141+
.output Value
142142

143143
.decl Heap(orig:Variable, item:Variable)
144-
.output Heap(delimiter=",")
144+
.output Heap
145145

146146
Heap(v,i) :- Store(v,i).
147147

@@ -258,39 +258,39 @@ Value(case_result, val) :-
258258
.decl VariableNodeTag(n:Variable, t:Tag)
259259
.decl VariableNodeParamType(n: Variable, t:Tag, i:number, nt:NodeParamType)
260260

261-
.output AbstractLocation(delimiter=",")
261+
.output AbstractLocation
262262
AbstractLocation(n) :- Heap(n,_).
263263

264-
.output VariableSimpleType(delimiter=",")
264+
.output VariableSimpleType
265265
VariableSimpleType(n,st) :- LitAssign(n,st,_).
266266
VariableSimpleType(n,"Unit") :- Update(n,_,_).
267267
VariableSimpleType(n,st) :- External(f,_,st), Call(n,f).
268268
VariableSimpleType(n,st) :- ExternalParam(f,i,st), Call(r,f), CallArgument(r,i,n).
269269
VariableSimpleType(n,st) :- Value(n,r), VariableSimpleType(r,st).
270270

271-
.output VariableNodeParamType(delimiter=",")
271+
.output VariableNodeParamType
272272
VariableNodeParamType(n,t,i,al)
273273
:- Node(n,t), NodeArgument(n,i,arg), Value(arg,al), AbstractLocation(al).
274274
VariableNodeParamType(n,t,i,st)
275275
:- Node(n,t), NodeArgument(n,i,arg), Value(arg,v), VariableSimpleType(v,st).
276276
VariableNodeParamType(n,t,i,ty)
277277
:- Value(n,n0), VariableNodeParamType(n0,t,i,ty).
278278

279-
.output VariableNodeTag(delimiter=",")
279+
.output VariableNodeTag
280280
VariableNodeTag(n,t) :- Value(n,r), Node(r,t).
281281

282-
.output VariableAbstractLocation(delimiter=",")
282+
.output VariableAbstractLocation
283283
VariableAbstractLocation(n,n) :- AbstractLocation(n).
284284
VariableAbstractLocation(n,v) :- Value(n,v), AbstractLocation(v).
285285

286286
.decl FunName(f: Function)
287-
.output FunName(delimiter=",")
287+
.output FunName
288288

289289
.decl FunReturn(f:Function, n:Variable)
290-
.output FunReturn(delimiter=",")
290+
.output FunReturn
291291

292292
.decl FunParam(f:Function, i:number, n:Variable)
293-
.output FunParam(delimiter=",")
293+
.output FunParam
294294

295295
FunName("main").
296296
FunName(f) :- Call(_,f), ReachableCode(f).
@@ -303,7 +303,7 @@ FunParam(f,i,p) :- ExternalParam(f,i,_), Call(r,f), CallArgument(r,i,p).
303303

304304
/* If a concrete instance of the abstract location may be subject to a fetch more than once, */
305305
.decl SharedLocation(n:Variable)
306-
.output SharedLocation(delimiter=",")
306+
// .output SharedLocation
307307

308308
SharedLocation(l) :-
309309
AbstractLocation(l), Value(v,l), NonLinearVar(v).
@@ -313,13 +313,13 @@ SharedLocation(l) :-
313313
//
314314

315315
.decl AfterInst(b:Variable,a:Variable)
316-
.output AfterInst(delimiter=",")
316+
// .output AfterInst
317317

318318
AfterInst(b,a) :- NextInst(b,a).
319319
AfterInst(b,c) :- AfterInst(b,a), NextInst(a,c).
320320

321321
.decl NonLinearVar(v:Variable)
322-
.output NonLinearVar(delimiter=",")
322+
// .output NonLinearVar
323323

324324
// Variable used in different use cases.
325325
// CA F M NP RV

0 commit comments

Comments
 (0)