diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-17 14:54:49 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-17 14:54:49 +0200 |
| commit | 613848182d167782fa5ee383b0e73b87e5ef1351 (patch) | |
| tree | 4745d5acd821e604d82510ebbc097863a271a10f /kvx/SelectOp.vp | |
| parent | 81a2cfe0971ca2456ff04c1e661b9a56279728ac (diff) | |
| download | compcert-kvx-613848182d167782fa5ee383b0e73b87e5ef1351.tar.gz compcert-kvx-613848182d167782fa5ee383b0e73b87e5ef1351.zip | |
Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1
Squashed commit of the following:
commit 808e72db2022d05a4e34818b33cc9af17aaa4df0
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:53:39 2021 +0200
selectOp for comp0
commit f38e1f15359cceb3c0764635336125a1ceae78ff
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:49:45 2021 +0200
SelectOp for ccomp0 ok
commit ca969280380a593aef590a1fe2ec6f0fc112c2f5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:46:01 2021 +0200
progress
commit e60a970f541ae6be30ec51cf95d60eb672ade829
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:40:49 2021 +0200
progres sur ltu etc.
commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:13:07 2021 +0200
change selection
commit c2af349c6dd3e09fec25f3a96e1272377b6450ef
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:03:31 2021 +0200
begin rewrite selector
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). |