From d2159e300b2d5e017a3144c747d34949b2ff2769 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 2 Feb 2021 10:21:17 +0100 Subject: begin implementing select --- riscV/Op.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'riscV/Op.v') diff --git a/riscV/Op.v b/riscV/Op.v index 21de7787..64d5e4c9 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -157,7 +157,8 @@ Inductive operation : Type := | Obits_of_single | Obits_of_float | Osingle_of_bits - | Ofloat_of_bits. + | Ofloat_of_bits + | Oselectl. (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -327,6 +328,7 @@ Definition eval_operation | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1) | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) | _, _ => None end. @@ -487,6 +489,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Obits_of_float => (Tfloat :: nil, Tlong) | Osingle_of_bits => (Tint :: nil, Tsingle) | Ofloat_of_bits => (Tlong :: nil, Tfloat) + | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -699,6 +702,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* single, float of bits *) - destruct v0; cbn; trivial. - destruct v0; cbn; trivial. + (* selectl *) + - destruct v0; cbn; trivial. + destruct Int.eq; cbn. + apply Val.normalize_type. + destruct Int.eq; cbn; trivial. + apply Val.normalize_type. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -1271,6 +1280,11 @@ Proof. (* single, double of bits *) - inv H4; simpl; auto. - inv H4; simpl; auto. + (* selectl *) + - inv H4; trivial. cbn. + destruct (Int.eq i Int.one). + + auto using Val.normalize_inject. + + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject. Qed. Lemma eval_addressing_inj: -- cgit