diff options
| -rw-r--r-- | src/common/IntegerExtra.v | 73 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 14 |
2 files changed, 83 insertions, 4 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index dcaf3a1..fe7d94f 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -199,7 +199,7 @@ Ltac ptrofs := end. Module IntExtra. - + Import Int. Ltac int_mod_match m := match goal with | [ H : ?x = 0 |- context[?x] ] => rewrite H @@ -291,4 +291,75 @@ Module IntExtra. rewrite <- Zmod_div_mod; try lia; try assumption end; try (crush; lia); int_mod_tac m. Qed. + + Definition ofbytes (a b c d : byte) : int := + or (shl (repr (Byte.unsigned a)) (repr (3 * Byte.zwordsize))) + (or (shl (repr (Byte.unsigned b)) (repr (2 * Byte.zwordsize))) + (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) + (repr (Byte.unsigned d)))). + + Definition byte1 (n: int) : byte := Byte.repr (unsigned n). + + Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))). + + Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))). + + Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))). + + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i. + Proof. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. + Qed. + + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize). + Proof. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. + change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. + apply zlt_true. omega. omega. + Qed. + + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)). + Proof. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. + change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). + apply zlt_true. omega. omega. + Qed. + + Lemma bits_byte4: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)). + Proof. + intros. unfold byte4. rewrite Byte.testbit_repr; auto. + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. + change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). + apply zlt_true. omega. omega. + Qed. + + Lemma bits_ofwords: + forall b4 b3 b2 b1 i, 0 <= i < zwordsize -> + testbit (ofbytes b4 b3 b2 b1) i = + if zlt i Byte.zwordsize + then Byte.testbit b1 i + else (if zlt i (2 * Byte.zwordsize) + then Byte.testbit b2 (i - Byte.zwordsize) + else (if zlt i (3 * Byte.zwordsize) + then Byte.testbit b2 (i - 2 * Byte.zwordsize) + else Byte.testbit b2 (i - 3 * Byte.zwordsize))). + Proof. + intros. unfold ofbytes. repeat (rewrite bits_or; auto). repeat (rewrite bits_shl; auto). + change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. + change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). + change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). + assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. + destruct (zlt i Byte.zwordsize). + rewrite testbit_repr; auto. + Abort. + End IntExtra. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 79bca49..82d4cfc 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -87,6 +87,12 @@ Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_frames_nil : match_frames nil nil. + Lemma assumption_32bit : + forall v, + valueToPos (posToValue v) = v. + Proof. + Admitted. + Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem m st res (MASSOC : match_assocmaps f rs asr) @@ -336,6 +342,7 @@ Section CORRECTNESS. intros (cu & tf & P & Q & R); exists tf; auto. Qed. + Lemma functions_translated: forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> @@ -398,6 +405,7 @@ Section CORRECTNESS. apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. apply Int.unsigned_range_2. + Admitted. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, @@ -406,7 +414,7 @@ Section CORRECTNESS. cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b -> - Verilog.expr_runp f asr asa c (boolToValue 32 b). + Verilog.expr_runp f asr asa c (boolToValue b). Admitted. (** The proof of semantic preservation for the translation of instructions @@ -436,7 +444,7 @@ Section CORRECTNESS. Ltac tac0 := match goal with - | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit + | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr @@ -456,7 +464,7 @@ Section CORRECTNESS. | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 | [ |- context[match_states _ _] ] => econstructor; auto | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto - | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] => + | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => |