Proof of fsval condition cmp ok

1 files changed, 52 insertions, 18 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 28760a72..cd74080f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -173,19 +173,19 @@ Inductive operation : Type :=
   (* Expansed conditions *)
   | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
-  | OEsequw (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
-  | OEsneuw (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequw (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneuw (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
   | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
   | OEsltiuw (n: int)                            (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
-  | OEluiw (n: int)                              (**r load upper-immediate *)
-  | OEaddiwr0 (n: int)                           (**r add immediate *)
+  | OEluiw (n: int) (is_long: bool)              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int) (is_long: bool)           (**r add immediate *)
   | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
-  | OEsequl (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
-  | OEsneul (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequl (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneul (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltl (optR0: option bool)                  (**r set-less-than *)
   | OEsltul (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltil (n: int64)                           (**r set-less-than immediate *)
@@ -263,6 +263,24 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v
   | Some false => sem v1 vz
   end.
 
+Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val :=
+  if negb is_long then
+    match v1 with
+    | Vint _ => sem vimm vz
+    | _ => Vundef
+    end
+  else
+    match v1 with
+    | Vlong _ => sem vimm vz
+    | _ => Vundef
+    end.
+
+Definition may_undef_luil (v1: val) (n: int64): val :=
+  match v1 with
+  | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
+  | _ => Vundef
+  end.
+
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -404,8 +422,8 @@ Definition eval_operation
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
   | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
-  | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12)))
-  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
+  | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12)))
+  | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32)
   | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
   | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64))
   | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
@@ -415,8 +433,8 @@ Definition eval_operation
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
   | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
   | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
-  | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
-  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
+  | OEluil n, v1::nil => Some (may_undef_luil v1 n)
+  | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64)
   | OEloadli n, nil => Some (Vlong n)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
@@ -605,8 +623,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltiw _ => (Tint :: nil, Tint)
   | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
-  | OEluiw _ => (nil, Tint)
-  | OEaddiwr0 _ => (nil, Tint)
+  | OEluiw _ _ => (Tint :: nil, Tint)
+  | OEaddiwr0 _ _ => (Tint :: nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
   | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
@@ -616,8 +634,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltil _ => (Tlong :: nil, Tint)
   | OEsltiul _ => (Tlong :: nil, Tint)
   | OExoril _ => (Tlong :: nil, Tlong)
-  | OEluil _ => (nil, Tlong)
-  | OEaddilr0 _ => (nil, Tlong)
+  | OEluil _ => (Tlong :: nil, Tlong)
+  | OEaddilr0 _ => (Tlong :: nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
@@ -857,9 +875,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoriw *)
   - destruct v0...
   (* OEluiw *)
-  - trivial.
+  - unfold may_undef_int;
+    destruct v0, is_long; simpl; trivial;
+    destruct (Int.ltu _ _); cbn; trivial.
   (* OEaddiwr0 *)
-  - trivial.
+  - destruct v0, is_long; simpl; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -886,9 +906,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoril *)
   - destruct v0...
   (* OEluil *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEaddilr0 *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEloadli *)
   - trivial.
   (* OEfeqd *)
@@ -1691,6 +1711,15 @@ Proof.
   - apply eval_cmpu_bool_inj; auto.
   (* OExoriw *)
   - inv H4; simpl; auto.
+  (* OEluiw *)
+  - unfold may_undef_int;
+    destruct is_long;
+    inv H4; simpl; auto;
+    destruct (Int.ltu _ _); auto.
+  (* OEaddiwr0 *)
+  - unfold may_undef_int;
+    destruct is_long;
+    inv H4; simpl; auto.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
@@ -1715,6 +1744,11 @@ Proof.
   - apply eval_cmplu_bool_inj; auto.
   (* OExoril *)
   - inv H4; simpl; auto.
+  (* OEluil *)
+  - inv H4; simpl; auto.
+  (* OEaddilr0 *)
+  - unfold may_undef_int;
+    inv H4; simpl; auto.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.