Created
March 27, 2024 21:11
-
-
Save jtpaasch/ee17028cb3ad76fb6f2592172555da69 to your computer and use it in GitHub Desktop.
Cousot's prefix trace semantics in (Souffle) datalog. Run the demos: `souffle -D- demo-01.dl` etc.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "library.dl" | |
// ========================================================= | |
// EXAMPLE | |
// ========================================================= | |
/* | |
------------------------------------------------------------ | |
THE PROGRAM | |
------------------------------------------------------------ | |
01 { | |
02 x = x + 1; | |
03 x = x + 1; | |
04 ; | |
05 } | |
------------------------------------------------------------ | |
THE AST | |
------------------------------------------------------------ | |
1 block | |
------------+-------- | |
/ | \ | |
/ | \ | |
/ | \ | |
/ | \ | |
/ 2 SL \ | |
/ +----------+---------+ | | |
/ | | | | |
| 3 SL 7 S | | |
| +--------+-------+ | | | |
| | | | | | |
| 4 SL 6 S | | | |
| +--+-+ | | | | |
| | | | | | | |
| 0 SL 5 S | | | | |
| | | | | | | |
{ - x = x + 1; x = x + 1; ; } | |
L02 L03 L04 Done | |
*/ | |
progEntry(1). | |
block(1,2). | |
stmtList(2,3,7). | |
stmtList(3,4,6). | |
stmtList(4,0,5). | |
valueStmt(5,"L02",500). | |
assignOpExpr(500,"=",501,502). | |
lvalExpr(501,"x"). | |
binOpExpr(502,"+",5021,5022). | |
readLvalExpr(5021,50211). | |
lvalExpr(50211,"x"). | |
intLitExpr(5022,"1"). | |
valueStmt(6,"L03",600). | |
assignOpExpr(600,"=",601,602). | |
lvalExpr(601,"x"). | |
binOpExpr(602,"+",6021,6022). | |
readLvalExpr(6021,60211). | |
lvalExpr(60211,"x"). | |
intLitExpr(6022,"1"). | |
valueStmt(7,"L04",700). | |
emptyExpr(700). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "library.dl" | |
// ========================================================= | |
// EXAMPLE | |
// ========================================================= | |
/* | |
------------------------------------------------------------ | |
THE PROGRAM | |
------------------------------------------------------------ | |
01 { | |
02 if (x < 3) { | |
03 y = 5; | |
04 } else { | |
05 ; | |
06 } | |
07 y = y + 1; | |
08 } | |
------------------------------------------------------------ | |
THE AST | |
------------------------------------------------------------ | |
1 block | |
+------------------+---------------------+ | |
/ | \ | |
/ 2 SL \ | |
/ +------------------+----------------------+ \ | |
/ | | \ | |
/ 3 SL 12 S \ | |
/ +-------+------+ | \ | |
| | | | | | |
| 0 SL 4 S | | | |
| | +----------+-----------+ | | | |
| | | | | | | |
| | | +----------+-----+--------------+ | | | |
| | | | | | | | | |
| | | 5 Bexpr 6 block 9 block | | | |
| | | | | | | | | |
| | | | 7 SL 10 SL | | | |
| | | | +--+-+ +--+-+ | | | |
| | | | | | | | | | | |
| | | | 0 SL 8 S 0 SL 11 S | | | |
| | | | | | | | | | | |
{ - if (x < 3) { - y = 5; } else { - ; } y = y + 1; } | |
L02 L03 L05 L06 Done | |
*/ | |
progEntry(1). | |
block(1,2). | |
stmtList(2,3,12). | |
stmtList(3,0,4). | |
ifStmt(4,"L02",5,6,9). | |
relOpExpr(5,"<",501,502). | |
readLvalExpr(501,5011). | |
lvalExpr(5011,"x"). | |
intLitExpr(502,"3"). | |
block(6,7). | |
stmtList(7,0,8). | |
valueStmt(8,"L03",800). | |
assignOpExpr(800,"=",801,802). | |
lvalExpr(801,"y"). | |
intLitExpr(802,"5"). | |
block(9,10). | |
stmtList(10,0,11). | |
valueStmt(11,"L05",1100). | |
emptyExpr(1100). | |
valueStmt(12,"L06",1200). | |
assignOpExpr(1200,"=",1201,1202). | |
lvalExpr(1201,"y"). | |
binOpExpr(1202,"+",120201,120202). | |
readLvalExpr(120201,1202011). | |
lvalExpr(1202011,"y"). | |
intLitExpr(120202,"1"). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "library.dl" | |
// ========================================================= | |
// EXAMPLE | |
// ========================================================= | |
/* | |
------------------------------------------------------------ | |
THE PROGRAM | |
------------------------------------------------------------ | |
01 { | |
02 y = 10; | |
03 while (x < 3) { | |
04 x = x + 1; | |
05 y = y + x; | |
06 } | |
07 {} | |
08 x = 0; | |
09 } | |
------------------------------------------------------------ | |
THE AST | |
------------------------------------------------------------ | |
1 block | |
+---------------------------------+--------------------+ | |
/ | \ | |
/ 2 SL \ | |
/ +-------+---------------------+ \ | |
/ | | \ | |
/ 3 SL 14 S | | |
| +---------------------+------------------------+ | | | |
| | | | | | |
| 4 SL 13 block | | | |
| +---------+----------+ +--+--+ | | | |
| | | | | | | | | |
| 5 SL 7 S |0 SL | | | | |
| +-+-+ +---------+------------+ | | | | | | |
| | | | | | | | | | | |
|0 SL 6 S | 8 block | | | | | | |
| | | | +------+----------+ | | | | | | |
| | | | / | \ | | | | | | |
| | | | / 9 SL \ | | | | | | |
| | | | | +------+------+ \ | | | | | | |
| | | | | | | | | | | | | | |
| | | | | 10 SL 12 S | | | | | | | |
| | | | | +-+-+ | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | |0 SL 11 S | | | | | | | | |
| | | | | | | | | | | | | | | |
{ - y = 10; while (x<3) { - x = x + 1; y = y + x; } { - } x = 0; } | |
L02 L03 L04 L05 L08 Done | |
*/ | |
progEntry(1). | |
block(1,2). | |
stmtList(2,3,14). | |
stmtList(3,4,13). | |
stmtList(4,5,7). | |
stmtList(5,0,6). | |
valueStmt(6,"L02",600). | |
assignOpExpr(600,"=",601,602). | |
lvalExpr(601,"y"). | |
intLitExpr(602,"10"). | |
whileStmt(7,"L03",700,8). | |
relOpExpr(700,"<",701,702). | |
readLvalExpr(701,7011). | |
lvalExpr(7011,"x"). | |
intLitExpr(702,"3"). | |
block(8,9). | |
stmtList(9,10,12). | |
stmtList(10,0,11). | |
valueStmt(11,"L04",1100). | |
assignOpExpr(1100,"=",1101,1102). | |
lvalExpr(1101,"x"). | |
binOpExpr(1102,"+",11021,11022). | |
readLvalExpr(11021,110211). | |
lvalExpr(110211,"x"). | |
intLitExpr(11022,"1"). | |
valueStmt(12,"L05",1200). | |
assignOpExpr(1200,"=",1201,1202). | |
lvalExpr(1201,"y"). | |
binOpExpr(1202,"+",12021,12022). | |
readLvalExpr(12021,120211). | |
lvalExpr(120211,"y"). | |
readLvalExpr(12022,120221). | |
lvalExpr(120221,"x"). | |
block(13,0). | |
valueStmt(14,"L08",1400). | |
assignOpExpr(1400,"=",1401,1402). | |
lvalExpr(1401,"x"). | |
intLitExpr(1402,"0"). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "library.dl" | |
// ========================================================= | |
// EXAMPLE | |
// ========================================================= | |
/* | |
------------------------------------------------------------ | |
THE PROGRAM | |
------------------------------------------------------------ | |
01 { | |
02 while (true) { | |
03 x = x + 1; | |
04 } | |
05 } | |
------------------------------------------------------------ | |
THE AST | |
------------------------------------------------------------ | |
1 block | |
+----+--------+ | |
/ | \ | |
/ 2 SL \ | |
| +----+----+ \ | |
| | | \ | |
| 0 SL 3 S \ | |
| | +-----+-----+ \ | |
| | | | \ | |
| | | +-----+------+ \ | |
| | | | | \ | |
| | | Bexpr 4 block \ | |
| | | | | \ | |
| | | | 5 SL | | |
| | | | +--+-+ | | |
| | | | | | | | |
| | | | 0 SL 6 S | | |
| | | | | | | | |
{ - while (true) { - x = x + 1; } | |
L02 L03 Done | |
*/ | |
progEntry(1). | |
block(1,2). | |
stmtList(2,0,3). | |
whileStmt(3,"L02",300,4). | |
boolLitExpr(300,"true"). | |
block(4,5). | |
stmtList(5,0,6). | |
valueStmt(6,"L03",600). | |
assignOpExpr(600,"=",601,602). | |
lvalExpr(601,"x"). | |
binOpExpr(602,"+",6021,6022). | |
readLvalExpr(6021,60211). | |
lvalExpr(60211,"x"). | |
intLitExpr(6022,"1"). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// ========================================================= | |
// Types | |
// ========================================================= | |
.type idx <: number // A generic id | |
.type ident <: symbol // Names (e.g., variables) | |
.type cp <: symbol // Control point (program label, e.g., "L02") | |
.type num <: symbol // Numeral (textual representation of a number) | |
.type bool <: symbol // "true" or "false" | |
.type binOp <: symbol // E.g., "+", etc. | |
.type assignOp <: symbol // E.g., "=", etc. | |
.type relOp <: symbol // E.g., "<", etc. | |
.type act <: symbol // Eg.., "skip","assgn", etc. | |
.type val <: number // Values are numbers | |
.type displayVal <: symbol // For displaying values | |
// ========================================================= | |
// Syntax | |
// ========================================================= | |
.decl intLitExpr(node:idx,num:num) | |
.decl lvalExpr(node:idx,var:ident) | |
.decl readLvalExpr(node:idx,lval:idx) | |
.decl emptyExpr(node:idx) | |
.decl boolLitExpr(node:idx,bool:bool) | |
.decl binOpExpr(node:idx,op:binOp,lhs:idx,rhs:idx) | |
.decl assignOpExpr(node:idx,op:assignOp,lhs:idx,rhs:idx) | |
.decl relOpExpr(node:idx,op:relOp,lhs:idx,rhs:idx) | |
.decl block(node:idx,body:idx) | |
.decl stmtList(node:idx,list:idx,stmt:idx) | |
.decl valueStmt(node:idx,cp:cp,expr:idx) | |
.decl ifStmt(node:idx,cp:cp,guard:idx,then:idx,else:idx) | |
.decl whileStmt(node:idx,cp:cp,guard:idx,body:idx) | |
.decl progEntry(node:idx) | |
.decl progVar(var:ident) | |
progVar(V) :- lvalExpr(_,V). | |
// ========================================================= | |
// Control points | |
// ========================================================= | |
.decl at(node:idx,cp:cp) | |
at(N,C) :- block(N,N1),at(N1,C). | |
at(N,C) :- block(N,0),after(N,C). | |
at(N,C) :- stmtList(N,0,N1),at(N1,C). | |
at(N,C) :- stmtList(N,N1,_),at(N1,C). | |
at(N,C) :- valueStmt(N,C,_). | |
at(N,C) :- ifStmt(N,C,_,_,_). | |
at(N,C) :- whileStmt(N,C,_,_). | |
.decl after(node:idx,cp:cp) | |
after(N,"Done") :- progEntry(N). | |
after(N,C) :- block(N1,N),after(N1,C),N>0. | |
after(N,C) :- stmtList(N1,_,N),after(N1,C). | |
after(N,C) :- stmtList(_,N,N1),at(N1,C),N>0. | |
after(N,C) :- ifStmt(N1,_,_,N,_),after(N1,C). | |
after(N,C) :- ifStmt(N1,_,_,_,N),after(N1,C). | |
after(N,C) :- whileStmt(N1,_,_,N),at(N1,C). | |
after(N,C) :- whileStmt(N,_,_,_),after(N,C). | |
// ========================================================= | |
// Traces | |
// ========================================================= | |
.decl trace(node:idx,trace:idx,head:idx,tail:cp) | |
.decl finTrace(node:idx,trace:idx,head:idx,tail:cp) | |
finTrace(N,T,T-1,C) :- trace(N,T,T-1,C),after(N,C). | |
.decl skipAction(node:idx,trace:idx,from:cp,to:cp) | |
.decl assignAction(node:idx,trace:idx,from:cp,to:cp,var:ident,val:val) | |
.decl noAssignAction(node:idx,trace:idx,from:cp,to:cp,var:ident) | |
.decl trueBranchAction(node:idx,trace:idx,from:cp,to:cp) | |
.decl falseBranchAction(node:idx,trace:idx,from:cp,to:cp) | |
.decl extendTrace(node:idx,trace:idx,with:idx) | |
trace(N1,T1+(T2-1),T1+(T2-2),C2) :- | |
extendTrace(N1,T1,N2), | |
trace(N1,T1,T1-1,C1),trace(N2,1,0,C1), | |
trace(N2,T2,T2-1,C2). | |
trace(N,1,0,C) :- valueStmt(N,C,_). | |
trace(N,T+1,T,C2) :- | |
trace(N,T,T-1,C1),valueStmt(N,C1,_),after(N,C2). | |
skipAction(N,T+1,C1,C2) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
valueStmt(_,C1,E),emptyExpr(E). | |
assignAction(N,T+1,C1,C2,V,Z) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
valueStmt(_,C1,E),assignOpExpr(E,"=",LHS,RHS), | |
lvalExpr(LHS,V),eval(N,T,RHS,Z). | |
noAssignAction(N,T+1,C1,C2,V) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
assignAction(N,T+1,C1,C2,V1,_), | |
progVar(V),V != V1. | |
trace(N,1,0,C) :- ifStmt(N,C,_,_,_). | |
trueBranchAction(N,T+1,C1,C2) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
ifStmt(_,C1,_,N1,_),at(N1,C2). | |
trace(N,T+1,T,C2) :- | |
trace(N,T,T-1,C1),ifStmt(N,C1,E,N1,_),at(N1,C2), | |
beval(N,T,E,"true"). | |
falseBranchAction(N,T+1,C1,C2) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
ifStmt(_,C1,_,_,N2),at(N2,C2). | |
trace(N,T+1,T,C2) :- | |
trace(N,T,T-1,C1),ifStmt(N,C1,E,_,N2),at(N2,C2), | |
beval(N,T,E,"false"). | |
extendTrace(N1,T,N2) :- | |
trueBranchAction(N1,T,C1,C2),at(N2,C2), | |
ifStmt(_,C1,_,N2,_),at(N2,C2). | |
extendTrace(N1,T,N2) :- | |
falseBranchAction(N1,T,C1,C2),at(N2,C2), | |
ifStmt(_,C1,_,_,N2),at(N2,C2). | |
extendTrace(N1,T,N2) :- | |
trueBranchAction(N1,T,C1,C2),at(N2,C2), | |
whileStmt(_,C1,_,N2),at(N2,C2). | |
trace(N,1,0,C) :- whileStmt(N,C,_,_). | |
trueBranchAction(N,T+1,C1,C2) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
whileStmt(_,C1,_,N1),at(N1,C2). | |
trace(N,T+1,T,C2) :- | |
trace(N,T,T-1,C1),whileStmt(N,C1,E,N1),at(N1,C2), | |
beval(N,T,E,"true"). | |
falseBranchAction(N,T+1,C1,C2) :- | |
trace(N,T,T-1,C1),trace(N,T+1,T,C2), | |
whileStmt(N1,C1,_,_),after(N1,C2). | |
trace(N,T+1,T,C2) :- | |
trace(N,T,T-1,C1),whileStmt(N,C1,E,_),after(N,C2), | |
beval(N,T,E,"false"). | |
trace(N,1,0,C) :- block(N,_),at(N,C). | |
extendTrace(N1,1,N2) :- | |
block(N1,N2),trace(N1,1,0,C),at(N2,C). | |
trace(N,1,0,C) :- stmtList(N,_,_),at(N,C). | |
extendTrace(N1,1,N2) :- | |
stmtList(N1,0,N2),trace(N1,1,0,C),at(N1,C). | |
extendTrace(N1,1,N2) :- | |
stmtList(N1,N2,_),trace(N1,1,0,C),at(N2,C). | |
extendTrace(N1,T,N3) :- | |
stmtList(N1,N2,N3), | |
trace(N1,T,T-1,C), | |
finTrace(N2,T,T-1,C), | |
at(N3,C). | |
// ========================================================= | |
// Machine configuration/state | |
// ========================================================= | |
.decl env(node:idx,trace:idx,var:ident,val:val) | |
env(N,1,V,0) :- trace(N,1,0,_),progVar(V). | |
env(N,T,V,Z) :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
assignAction(N,T,C1,C2,V,Z). | |
env(N,T,V,Z) :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
noAssignAction(N,T,C1,C2,V),env(N,T-1,V,Z). | |
env(N,T,V,Z) :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
skipAction(N,T,C1,C2),env(N,T-1,V,Z). | |
env(N,T,V,Z) :- | |
trace(N,T,T-1,_),trace(N,T-1,_,C1), | |
!valueStmt(_,C1,_),env(N,T-1,V,Z). | |
.decl eval(node:idx,trace:idx,expr:idx,val:val) | |
eval(N,T,E,Z) :- | |
trace(N,T,T-1,_),lvalExpr(E,V),env(N,T,V,Z). | |
eval(N,T,E,Z) :- | |
trace(N,T,_,_),intLitExpr(E,Z1),Z = to_number(Z1). | |
eval(N,T,E,Z) :- | |
trace(N,T,T-1,_),readLvalExpr(E,E1),eval(N,T,E1,Z). | |
eval(N,T,E,Z) :- | |
trace(N,T,T-1,_),binOpExpr(E,"+",LHS,RHS), | |
eval(N,T,LHS,Z1),eval(N,T,RHS,Z2),Z = Z1 + Z2. | |
.decl beval(node:idx,trace:idx,expr:idx,bool:bool) | |
beval(N,T,E,B) :- | |
trace(N,T,T-1,_),boolLitExpr(E,B). | |
beval(N,T,E,"true") :- | |
trace(N,T,T-1,_),relOpExpr(E,"<",LHS,RHS), | |
eval(N,T,LHS,Z1),eval(N,T,RHS,Z2), | |
Z1 < Z2. | |
beval(N,T,E,"false") :- | |
trace(N,T,T-1,_),relOpExpr(E,"<",LHS,RHS), | |
eval(N,T,LHS,Z1),eval(N,T,RHS,Z2), | |
Z1 >= Z2. | |
// ========================================================= | |
// Trace summary | |
// ========================================================= | |
.decl traceSummary(node:idx,trace:idx, | |
from:cp,act:act,to:cp,var:ident,val:displayVal) | |
traceSummary(N,1,C,"-","-","-","-") :- trace(N,1,0,C). | |
traceSummary(N,T,C1,"skip",C2,"-","-") :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1),skipAction(N,T,C1,C2). | |
traceSummary(N,T,C1,"assgn",C2,V,Z) :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
assignAction(N,T,C1,C2,V,Z1),Z = to_string(Z1). | |
traceSummary(N,T,C1,"tt",C2,"-","-") :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
trueBranchAction(N,T,C1,C2). | |
traceSummary(N,T,C1,"ff",C2,"-","-") :- | |
trace(N,T,T-1,C2),trace(N,T-1,_,C1), | |
falseBranchAction(N,T,C1,C2). | |
// ========================================================= | |
// Output | |
// ========================================================= | |
// .output at | |
// .output after | |
// .output extendTrace | |
// .output trace | |
// .output finTrace | |
// .output skipAction | |
// .output assignAction | |
// .output noAssignAction | |
// .output trueBranchAction | |
// .output falseBranchAction | |
// .output env | |
// .output eval | |
// .output beval | |
.output traceSummary |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment