Skip to content

Add metadata to unstructured programs #1147

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
PROgram52bc wants to merge 1 commit into from
Closed

Add metadata to unstructured programs #1147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Strata/DL/Imperative/BasicBlock.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ inductive DetTransferCmd (Label : Type) (P : PureExpr) where
model it instead using `condGoto`. By defining this function, we can easily
create unconditional jumps, and future proof against the possibility of adding
it as a constructor in the future. -/
def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P :=
condGoto HasBool.tt l l
def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P := .empty) : DetTransferCmd Label P :=
condGoto HasBool.tt l l md

/-- A `NondetTransfer` command terminates a non-deterministic basic block,
indicating the list of possible blocks where execution could proceed next, if
Expand Down
18 changes: 9 additions & 9 deletions Strata/Transform/StructuredToUnstructured.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ match ss with
| .typeDecl _ _ :: rest => do
-- Not yet supported, so just continue with `rest`.
stmtsToBlocks k rest exitConts accum
| .block l bss _md :: rest => do
| .block l bss md :: rest => do
-- Process rest first
let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
-- Process block body, extending the list of exit continuations.
Expand All @@ -77,9 +77,9 @@ match ss with
-- Empty accumulated block
pure (accumEntry, accumBlocks ++ bbs ++ bsNext)
else
let b := (l, { cmds := [], transfer := .goto bl })
let b := (l, { cmds := [], transfer := .goto bl md })
pure (l, accumBlocks ++ [b] ++ bbs ++ bsNext)
| .ite c tss fss _md :: rest => do
| .ite c tss fss md :: rest => do
-- Process rest first
let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
-- Create ite block
Expand All @@ -95,9 +95,9 @@ match ss with
let initCmd := HasInit.init ident HasBool.boolTy .nondet MetaData.empty
pure (HasFvar.mkFvar ident, [initCmd])
let (accumEntry, accumBlocks) ← flushCmds "ite$" (accum ++ extraCmds)
(.some (.condGoto condExpr tl fl)) l
(.some (.condGoto condExpr tl fl md)) l
pure (accumEntry, accumBlocks ++ tbs ++ fbs ++ bsNext)
| .loop c m is bss _md :: rest => do
| .loop c m is bss md :: rest => do
-- Process rest first
let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
-- Create loop entry block
Expand Down Expand Up @@ -135,18 +135,18 @@ match ss with
-- For nondet guards, introduce a fresh boolean variable
match c with
| .det e =>
let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext })
let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext md })
let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
| .nondet => do
let freshName ← StringGenState.gen "$__nondet_loop$"
let ident := HasIdent.ident (P := P) freshName
let initCmd := HasInit.init ident HasBool.boolTy .nondet MetaData.empty
let b := (lentry, { cmds := [initCmd] ++ invCmds ++ measureCmds,
transfer := .condGoto (HasFvar.mkFvar ident) bl kNext })
transfer := .condGoto (HasFvar.mkFvar ident) bl kNext md })
let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
| .exit l? _md :: _ => do
| .exit l? md :: _ => do
-- Find the continuation of the block labeled `l`, or the most recently-added
-- block if `l` is `.none`.
let bk :=
Expand All @@ -167,7 +167,7 @@ match ss with
match l? with
| .some l => s!"block${l}$"
| .none => "block$"
flushCmds exitName accum .none bk
flushCmds exitName accum (.some (.goto bk md)) bk

def stmtsToCFGM
[HasBool P] [HasPassiveCmds P CmdT] [HasInit P CmdT]
Expand Down
22 changes: 11 additions & 11 deletions StrataTest/Languages/Core/Examples/Exit.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,10 +116,10 @@ Result: ✅ pass
info: Entry: l1

l1:
condGoto true block$l1$_2 block$l1$_2
#[<[fileRange]: :387-502>] condGoto true block$l1$_2 block$l1$_2
block$l1$_2:
assert [a1]: x == x;
condGoto true l$_1 l$_1
#[<[fileRange]: :426-434>] condGoto true l$_1 l$_1
l$_1:
assert [a3]: x == x;
condGoto true end$_0 end$_0
Expand All @@ -133,29 +133,29 @@ end$_0:
info: Entry: l5

l5:
condGoto true l4 l4
#[<[fileRange]: :577-1056>] condGoto true l4 l4
l4:
condGoto true l4_before l4_before
#[<[fileRange]: :589-1050>] condGoto true l4_before l4_before
l4_before:
condGoto true l3_before l3_before
#[<[fileRange]: :603-996>] condGoto true l3_before l3_before
l3_before:
condGoto true l1 l1
#[<[fileRange]: :626-933>] condGoto true l1 l1
l1:
condGoto true ite$_5 ite$_5
#[<[fileRange]: :651-835>] condGoto true ite$_5 ite$_5
ite$_5:
assert [a4]: x == x;
condGoto x > 0 block$l5$_2 block$l5$_1
#[<[fileRange]: :706-821>] condGoto x > 0 block$l5$_2 block$l5$_1
l2:
condGoto true l$_3 l$_3
#[<[fileRange]: :848-921>] condGoto true l$_3 l$_3
l$_3:
assert [a5]: !(x == x);
condGoto true block$l5$_2 block$l5$_2
block$l5$_2:
assert [a6]: x * 2 > x;
condGoto true end$_0 end$_0
#[<[fileRange]: :978-986>] condGoto true end$_0 end$_0
block$l5$_1:
assert [a7]: x <= 0;
condGoto true end$_0 end$_0
#[<[fileRange]: :1034-1042>] condGoto true end$_0 end$_0
end$_0:
finish
-/
Expand Down
8 changes: 4 additions & 4 deletions StrataTest/Languages/Core/Examples/Loops.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ loop_entry$_1:
var loop_measure$_2 : int;
assume [assume_loop_measure$_2]: loop_measure$_2 == n;
assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
condGoto i < n l$_4 end$_0
#[<[fileRange]: :813-919>] condGoto i < n l$_4 end$_0
l$_4:
i := i + 1;
condGoto true measure_decrease$_3 measure_decrease$_3
Expand Down Expand Up @@ -140,7 +140,7 @@ loop_entry$_1:
var loop_measure$_2 : int;
assume [assume_loop_measure$_2]: loop_measure$_2 == n - i;
assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
condGoto i < n l$_4 end$_0
#[<[fileRange]: :2438-2594>] condGoto i < n l$_4 end$_0
l$_4:
i := i + 1;
s := s + i;
Expand Down Expand Up @@ -387,7 +387,7 @@ Context: Global scope:
var loop_measure$_2 : int;
assume [assume_loop_measure$_2]: loop_measure$_2 == n - x;
assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
condGoto x < n before_loop$_11 end$_0
#[<[fileRange]: :8059-8312>] condGoto x < n before_loop$_11 end$_0
before_loop$_11:
y := 0;
condGoto true loop_entry$_5 loop_entry$_5
Expand All @@ -397,7 +397,7 @@ loop_entry$_5:
var loop_measure$_6 : int;
assume [assume_loop_measure$_6]: loop_measure$_6 == x - y;
assert [measure_lb_loop_measure$_6]: !(loop_measure$_6 < 0);
condGoto y < x l$_8 l$_4
#[<[fileRange]: :8179-8292>] condGoto y < x l$_8 l$_4
l$_8:
y := y + 1;
condGoto true measure_decrease$_7 measure_decrease$_7
Expand Down
Loading