Commit f3f108af authored by Benedikt Geßele's avatar Benedikt Geßele

liveness: use two instead of one iteration to optimize while loops

parent e470f7cb
......@@ -12,7 +12,7 @@ GDSL_MEX=_manual
GDSL_COMP=$(GDSL)$(GDSL_MEX)
GDSL_EXEC=$(GDSL)c
GPREFIX=
#GDSLFLAGS=
GDSLFLAGS=--maxIter=42
#GDSL_SOURCES=$(shell find specifications/basis specifications/rreil specifications/x86 -type f -name '*.ml')
GDSL_BASIS_HL=specifications/basis/prelude.ml specifications/basis/bbtree.ml specifications/basis/tree-set.ml
......
......@@ -212,7 +212,7 @@ val lv-pretty t =
val live-stack-backup-and-reset = do
live <- query $live;
maybelive <- query $live;
maybelive <- query $live; # sure that it's not maybelive?
update @{live=SEM_NIL,maybelive=SEM_NIL};
return {live=live,maybelive=maybelive}
end
......@@ -253,15 +253,19 @@ val lv-analyze initial-live stack =
backup <- live-stack-backup-and-reset;
body-rev <- return (rreil-stmts-rev y.body);
body-state <- sweep body-rev (lvstate-empty fmap-empty body-rev);
state-new <- return (lvstate-union-conservative state body-state);
first-it-state <- sweep body-rev (lvstate-empty initial-live body-rev);
live-stack-backup-and-reset;
second-it-state <- sweep body-rev (lvstate-union (lvstate-eval state x.hd) first-it-state);
# state-new <- return (lvstate-union-conservative state body-state);
body-live <- query $live;
#maybelive <- query $maybelive;
live-stack-restore backup;
#lv-push-live (/WHILE y.cond maybelive);
lv-push-live (/WHILE y.cond y.body);
sweep x.tl (lvstate-eval state-new x.hd)
lv-push-live (/WHILE y.cond body-live);
sweep x.tl (lvstate-eval second-it-state x.hd)
end
| SEM_ITE y: do
org-backup <- live-stack-backup-and-reset;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment