diff options
Diffstat (limited to 'kvx/SelectOp.vp')
| -rw-r--r-- | kvx/SelectOp.vp | 44 |
1 files changed, 33 insertions, 11 deletions
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index aa241c1e..16607cf5 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -64,29 +64,49 @@ Section SELECT. Context {hf: helper_functions}. +Inductive to_cond0 := +| Cond0_some : condition0 -> expr -> to_cond0 +| Cond0_none : to_cond0 +| Cond0_true : to_cond0 +| Cond0_false : to_cond0. + +Definition compu0 c e1 := + match c with + | Clt => Cond0_false + | Cge => Cond0_true + | _ => Cond0_some (Ccompu0 c) e1 + end. + +Definition complu0 c e1 := + match c with + | Clt => Cond0_false + | Cge => Cond0_true + | _ => Cond0_some (Ccomplu0 c) e1 + end. + Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) := match cond, args with | (Ccompimm c x), (e1 ::: Enil) => if Int.eq_dec x Int.zero - then Some ((Ccomp0 c), e1) - else None + then Cond0_some (Ccomp0 c) e1 + else Cond0_none | (Ccompuimm c x), (e1 ::: Enil) => if Int.eq_dec x Int.zero - then Some ((Ccompu0 c), e1) - else None + then compu0 c e1 + else Cond0_none | (Ccomplimm c x), (e1 ::: Enil) => if Int64.eq_dec x Int64.zero - then Some ((Ccompl0 c), e1) - else None + then Cond0_some (Ccompl0 c) e1 + else Cond0_none | (Ccompluimm c x), (e1 ::: Enil) => if Int64.eq_dec x Int64.zero - then Some ((Ccomplu0 c), e1) - else None + then complu0 c e1 + else Cond0_none - | _, _ => None + | _, _ => Cond0_none end. (** Ternary operator *) @@ -112,8 +132,10 @@ Definition same_expr_pure (e1 e2: expr) := Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := Some (if same_expr_pure e1 e2 then e1 else match cond_to_condition0 cond args with - | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args) - | Some(cond0, ec) => select0 ty cond0 e1 e2 ec + | Cond0_none => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args) + | Cond0_some cond0 ec => select0 ty cond0 e1 e2 ec + | Cond0_true => e1 + | Cond0_false => e2 end). |