Skip to content

Instantly share code, notes, and snippets.

@jtpaasch

jtpaasch/demo-01.dl

Created March 27, 2024 21:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jtpaasch/ee17028cb3ad76fb6f2592172555da69 to your computer and use it in GitHub Desktop.
Save jtpaasch/ee17028cb3ad76fb6f2592172555da69 to your computer and use it in GitHub Desktop.
Download ZIP
Cousot's prefix trace semantics in (Souffle) datalog. Run the demos: `souffle -D- demo-01.dl` etc.
Raw
demo-01.dl
#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).
Raw
demo-02.dl
#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").
Raw
demo-03.dl
#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").
Raw
demo-04.dl
#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").
Raw
library.dl
// =========================================================
// 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