Skip to content
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

Jump to bottom

simplify expr metrics WIP #70

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

simplify expr metrics WIP #70

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
96 changes: 39 additions & 57 deletions bedrock2/src/Semantics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,50 +126,32 @@ Section semantics.

Section WithMemAndLocals.
Context (m : mem) (l : locals).
Fixpoint eval_expr (e : expr) (mc : metrics) : option (word * metrics) :=
match e with
| expr.literal v => Some (word.of_Z v, addMetricInstructions 8
(addMetricLoads 8 mc))
| expr.var x => match map.get l x with
| Some v => Some (v, addMetricInstructions 1
(addMetricLoads 2 mc))
| None => None
end
| expr.load aSize a =>
'Some (a', mc') <- eval_expr a mc | None;
'Some v <- load aSize m a' | None;
Some (v, addMetricInstructions 1
(addMetricLoads 2 mc'))
| expr.op op e1 e2 =>
'Some (v1, mc') <- eval_expr e1 mc | None;
'Some (v2, mc'') <- eval_expr e2 mc' | None;
Some (interp_binop op v1 v2, addMetricInstructions 2
(addMetricLoads 2 mc''))
end.

Fixpoint eval_expr_old (e : expr) : option word :=
Fixpoint eval_expr (e : expr) : option word :=
match e with
| expr.literal v => Some (word.of_Z v)
| expr.var x => map.get l x
| expr.load aSize a =>
'Some a' <- eval_expr_old a | None;
'Some a' <- eval_expr a | None;
load aSize m a'
| expr.op op e1 e2 =>
'Some v1 <- eval_expr_old e1 | None;
'Some v2 <- eval_expr_old e2 | None;
'Some v1 <- eval_expr e1 | None;
'Some v2 <- eval_expr e2 | None;
Some (interp_binop op v1 v2)
end.

Fixpoint evaluate_call_args_log (arges : list expr) (mc : metrics) :=
match arges with
| e :: tl =>
'Some (v, mc') <- eval_expr e mc | None;
'Some (args, mc'') <- evaluate_call_args_log tl mc' | None;
Some (v :: args, mc'')
| _ => Some (nil, mc)
end.

End WithMemAndLocals.

Fixpoint measure_expr (e : expr) (mc : metrics) : metrics :=
match e with
| expr.literal v => addMetricInstructions 8 (addMetricLoads 8 mc)
| expr.var x => addMetricInstructions 1 (addMetricLoads 2 mc)
| expr.load aSize a => addMetricInstructions 1 (addMetricLoads 2 (measure_expr a mc))
| expr.op op e1 e2 => addMetricInstructions 2 (addMetricLoads 2 (measure_expr e2 (measure_expr e1 mc)))
end.
Fixpoint measure_args (arges : list expr) (mc : metrics) :=
match arges with
| e :: tl => measure_args tl (measure_expr e mc)
| _ => mc
end.
End semantics.

Module exec. Section WithEnv.
Expand All @@ -187,37 +169,37 @@ Module exec. Section WithEnv.
: exec cmd.skip t m l mc post
| set x e
t m l mc post
v mc' (_ : eval_expr m l e mc = Some (v, mc'))
v (_ : eval_expr m l e = Some v)
(_ : post t m (map.put l x v) (addMetricInstructions 1
(addMetricLoads 1 mc')))
(addMetricLoads 1 (measure_expr e mc))))
: exec (cmd.set x e) t m l mc post
| unset x
t m l mc post
(_ : post t m (map.remove l x) mc)
: exec (cmd.unset x) t m l mc post
| store sz ea ev
t m l mc post
a mc' (_ : eval_expr m l ea mc = Some (a, mc'))
v mc'' (_ : eval_expr m l ev mc' = Some (v, mc''))
a (_ : eval_expr m l ea = Some a)
v (_ : eval_expr m l ev = Some v)
m' (_ : store sz m a v = Some m')
(_ : post t m' l (addMetricInstructions 1
(addMetricLoads 1
(addMetricStores 1 mc''))))
(addMetricStores 1 (measure_expr ev (measure_expr ea mc))))))
: exec (cmd.store sz ea ev) t m l mc post
| if_true t m l mc e c1 c2 post
v mc' (_ : eval_expr m l e mc = Some (v, mc'))
v (_ : eval_expr m l e = Some v)
(_ : word.unsigned v <> 0)
(_ : exec c1 t m l (addMetricInstructions 2
(addMetricLoads 2
(addMetricJumps 1 mc'))) post)
(addMetricJumps 1 (measure_expr e mc)))) post)
: exec (cmd.cond e c1 c2) t m l mc post
| if_false e c1 c2
t m l mc post
v mc' (_ : eval_expr m l e mc = Some (v, mc'))
v (_ : eval_expr m l e = Some v)
(_ : word.unsigned v = 0)
(_ : exec c2 t m l (addMetricInstructions 2
(addMetricLoads 2
(addMetricJumps 1 mc'))) post)
(addMetricJumps 1 (measure_expr e mc)))) post)
: exec (cmd.cond e c1 c2) t m l mc post
| seq c1 c2
t m l mc post
Expand All @@ -226,47 +208,47 @@ Module exec. Section WithEnv.
: exec (cmd.seq c1 c2) t m l mc post
| while_false e c
t m l mc post
v mc' (_ : eval_expr m l e mc = Some (v, mc'))
v (_ : eval_expr m l e = Some v)
(_ : word.unsigned v = 0)
(_ : post t m l (addMetricInstructions 1
(addMetricLoads 1
(addMetricJumps 1 mc'))))
(addMetricJumps 1 (measure_expr e mc)))))
: exec (cmd.while e c) t m l mc post
| while_true e c
t m l mc post
v mc' (_ : eval_expr m l e mc = Some (v, mc'))
v (_ : eval_expr m l e = Some v)
(_ : word.unsigned v <> 0)
mid (_ : exec c t m l mc' mid)
(_ : forall t' m' l' mc'', mid t' m' l' mc'' ->
mid (_ : exec c t m l (measure_expr e mc) mid)
(_ : forall t' m' l' mc', mid t' m' l' mc' ->
exec (cmd.while e c) t' m' l' (addMetricInstructions 2
(addMetricLoads 2
(addMetricJumps 1 mc''))) post)
(addMetricJumps 1 mc'))) post)
: exec (cmd.while e c) t m l mc post
| call binds fname arges
t m l mc post
params rets fbody (_ : map.get e fname = Some (params, rets, fbody))
args mc' (_ : evaluate_call_args_log m l arges mc = Some (args, mc'))
args (_ : List.option_all (List.map (eval_expr m l) arges) = Some args)
lf (_ : map.putmany_of_list params args map.empty = Some lf)
mid (_ : exec fbody t m lf mc' mid)
(_ : forall t' m' st1 mc'', mid t' m' st1 mc'' ->
mid (_ : exec fbody t m lf (measure_args arges mc) mid)
(_ : forall t' m' st1 mc', mid t' m' st1 mc' ->
exists retvs, map.getmany_of_list st1 rets = Some retvs /\
exists l', map.putmany_of_list binds retvs l = Some l' /\
post t' m' l' mc'')
post t' m' l' mc')
: exec (cmd.call binds fname arges) t m l mc post
| interact binds action arges
t m l mc post
mKeep mGive (_: map.split m mKeep mGive)
args mc' (_ : evaluate_call_args_log m l arges mc = Some (args, mc'))
args (_ : List.option_all (List.map (eval_expr m l) arges) = Some args)
mid (_ : ext_spec t mGive action args mid)
(_ : forall mReceive resvals, mid mReceive resvals ->
exists l', map.putmany_of_list binds resvals l = Some l' /\
exists m', map.split m' mKeep mReceive /\
post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l'
(addMetricInstructions 1
(addMetricStores 1
(addMetricLoads 2 mc'))))
(addMetricLoads 2 (measure_args arges mc)))))
: exec (cmd.interact binds action arges) t m l mc post
.
End WithEnv.
Arguments exec {_} _.
End exec. Notation exec := exec.exec.
End exec. Notation exec := exec.exec.
15 changes: 6 additions & 9 deletions bedrock2/src/WeakestPreconditionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,22 +179,19 @@ Section WeakestPrecondition.
| _ => progress cbv [dlet.dlet WeakestPrecondition.dexpr WeakestPrecondition.dexprs WeakestPrecondition.store] in *
end; eauto.

Lemma expr_sound m l e mc post (H : WeakestPrecondition.expr m l e post)
: exists v mc', Semantics.eval_expr m l e mc = Some (v, mc') /\ post v.
Lemma expr_sound m l e post (H : WeakestPrecondition.expr m l e post)
: exists v, Semantics.eval_expr m l e = Some v /\ post v.
Proof.
ind_on Syntax.expr; t.
{ destruct H. destruct H. eexists. eexists. rewrite H. eauto. }
{ eapply IHe in H; t. cbv [WeakestPrecondition.load] in H0; t. rewrite H. rewrite H0. eauto. }
{ eapply IHe in H; eauto. destruct H. destruct H. setoid_rewrite H. eauto. }
{ eapply IHe1 in H; t. eapply IHe2 in H0; t. rewrite H, H0; eauto. }
Qed.

Lemma sound_args : forall m l args mc P,
Lemma sound_args : forall m l args P,
WeakestPrecondition.list_map (WeakestPrecondition.expr m l) args P ->
exists x mc',
Semantics.evaluate_call_args_log m l args mc = Some (x, mc') /\ P x.
exists x, List.option_all (List.map (Semantics.eval_expr m l) args) = Some x /\ P x.
Proof.
induction args; cbn; repeat (subst; t).
unfold Semantics.eval_expr in *.
eapply expr_sound in H; t; rewrite H.
eapply IHargs in H0; t; rewrite H0.
eauto.
Expand All @@ -204,7 +201,7 @@ Section WeakestPrecondition.
Lemma sound_nil c t m l mc post
(H:WeakestPrecondition.cmd (fun _ _ _ _ _ => False) c t m l post)
: Semantics.exec map.empty c t m l mc (fun t' m' l' mc' => post t' m' l').
Proof.
Proof.
ind_on Syntax.cmd; repeat (t; try match reverse goal with H : WeakestPrecondition.expr _ _ _ _ |- _ => eapply expr_sound in H end).
{ destruct (BinInt.Z.eq_dec (Interface.word.unsigned x) (BinNums.Z0)) as [Hb|Hb]; cycle 1.
{ econstructor; t. }
Expand Down
24 changes: 12 additions & 12 deletions compiler/src/ExprImp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,20 +46,20 @@ Section ExprImp1.
| O => None (* out of fuel *)
| S f => match s with
| cmd.store aSize a v =>
'Some a <- eval_expr_old m st a;
'Some v <- eval_expr_old m st v;
'Some a <- eval_expr m st a;
'Some v <- eval_expr m st v;
'Some m <- store aSize m a v;
Some (st, m)
| cmd.set x e =>
'Some v <- eval_expr_old m st e;
'Some v <- eval_expr m st e;
Some (map.put st x v, m)
| cmd.unset x =>
Some (map.remove st x, m)
| cmd.cond cond bThen bElse =>
'Some v <- eval_expr_old m st cond;
'Some v <- eval_expr m st cond;
eval_cmd f st m (if word.eqb v (word.of_Z 0) then bElse else bThen)
| cmd.while cond body =>
'Some v <- eval_expr_old m st cond;
'Some v <- eval_expr m st cond;
if word.eqb v (word.of_Z 0) then Some (st, m) else
'Some (st, m) <- eval_cmd f st m body;
eval_cmd f st m (cmd.while cond body)
Expand All @@ -69,7 +69,7 @@ Section ExprImp1.
| cmd.skip => Some (st, m)
| cmd.call binds fname args =>
'Some (params, rets, fbody) <- map.get e fname;
'Some argvs <- List.option_all (List.map (eval_expr_old m st) args);
'Some argvs <- List.option_all (List.map (eval_expr m st) args);
'Some st0 <- map.putmany_of_list params argvs map.empty;
'Some (st1, m') <- eval_cmd f st0 m fbody;
'Some retvs <- map.getmany_of_list st1 rets;
Expand Down Expand Up @@ -139,15 +139,15 @@ Section ExprImp1.

Lemma invert_eval_store: forall fuel initialSt initialM a v final aSize,
eval_cmd (S fuel) initialSt initialM (cmd.store aSize a v) = Some final ->
exists av vv finalM, eval_expr_old initialM initialSt a = Some av /\
eval_expr_old initialM initialSt v = Some vv /\
exists av vv finalM, eval_expr initialM initialSt a = Some av /\
eval_expr initialM initialSt v = Some vv /\
store aSize initialM av vv = Some finalM /\
final = (initialSt, finalM).
Proof. inversion_lemma. Qed.

Lemma invert_eval_set: forall f st1 m1 p2 x e,
eval_cmd (S f) st1 m1 (cmd.set x e) = Some p2 ->
exists v, eval_expr_old m1 st1 e = Some v /\ p2 = (map.put st1 x v, m1).
exists v, eval_expr m1 st1 e = Some v /\ p2 = (map.put st1 x v, m1).
Proof. inversion_lemma. Qed.

Lemma invert_eval_unset: forall f st1 m1 p2 x,
Expand All @@ -158,15 +158,15 @@ Section ExprImp1.
Lemma invert_eval_cond: forall f st1 m1 p2 cond bThen bElse,
eval_cmd (S f) st1 m1 (cmd.cond cond bThen bElse) = Some p2 ->
exists cv,
eval_expr_old m1 st1 cond = Some cv /\
eval_expr m1 st1 cond = Some cv /\
(cv <> word.of_Z 0 /\ eval_cmd f st1 m1 bThen = Some p2 \/
cv = word.of_Z 0 /\ eval_cmd f st1 m1 bElse = Some p2).
Proof. inversion_lemma. Qed.

Lemma invert_eval_while: forall st1 m1 p3 f cond body,
eval_cmd (S f) st1 m1 (cmd.while cond body) = Some p3 ->
exists cv,
eval_expr_old m1 st1 cond = Some cv /\
eval_expr m1 st1 cond = Some cv /\
(cv <> word.of_Z 0 /\ (exists st2 m2, eval_cmd f st1 m1 body = Some (st2, m2) /\
eval_cmd f st2 m2 (cmd.while cond body) = Some p3) \/
cv = word.of_Z 0 /\ p3 = (st1, m1)).
Expand All @@ -186,7 +186,7 @@ Section ExprImp1.
eval_cmd (S f) st m1 (cmd.call binds fname args) = Some p2 ->
exists params rets fbody argvs st0 st1 m' retvs st',
map.get e fname = Some (params, rets, fbody) /\
List.option_all (List.map (eval_expr_old m1 st) args) = Some argvs /\
List.option_all (List.map (eval_expr m1 st) args) = Some argvs /\
map.putmany_of_list params argvs map.empty = Some st0 /\
eval_cmd f st0 m1 fbody = Some (st1, m') /\
map.getmany_of_list st1 rets = Some retvs /\
Expand Down