From a23cc48f449ffbfd347f833965c1e04b88e0009a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 Jun 2020 14:12:38 +0100 Subject: Add more unproven instructions, Admitted equiv to spec --- src/translation/HTLgen.v | 43 ++++++++++++++++++++++++------------------- src/translation/HTLgenspec.v | 4 ++-- src/verilog/PrintVerilog.ml | 3 ++- src/verilog/Verilog.v | 4 +++- 4 files changed, 31 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 96ac8df..11580cd 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -219,7 +219,7 @@ Definition translate_comparison (c : Integers.comparison) (args : list reg) : mo | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) - | _, _ => error (Errors.msg "Veriloggen: comparison instruction not implemented: other") + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") end. Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) @@ -231,7 +231,7 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) | Integers.Cle, r1::nil => ret (boplit Vle r1 i) | Integers.Cge, r1::nil => ret (boplit Vge r1 i) - | _, _ => error (Errors.msg "Veriloggen: comparison_imm instruction not implemented: other") + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") end. Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := @@ -240,9 +240,9 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | Op.Ccompu c, _ => translate_comparison c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero") - | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero") - | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other") + | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") + | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := @@ -257,7 +257,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) ret (Vlit (ZToValue 32 a)) - | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other") + | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") end. (** Translate an instruction to a statement. *) @@ -269,8 +269,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs") - | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu") + | Op.Omulhs, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhs") + | Op.Omulhu, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhu") | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) @@ -286,16 +286,21 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm") - | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru") - | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm") - | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm") - | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm") + | Op.Oshrximm n, r::nil => ret (Vbinop Vdiv (Vvar r) + (Vbinop Vshl (Vlit (ZToValue 32 1)) + (Vlit (intToValue n)))) + | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) + | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + | Op.Oshldimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshldimm") | Op.Ocmp c, _ => translate_condition c args + | Op.Osel c AST.Tint, r1::r2::rl => + do tc <- translate_condition c rl; + ret (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *) | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *) - | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other") + | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. Lemma add_branch_instr_state_incr: @@ -329,7 +334,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := (AssocMap.set n Vskip (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) - | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr") + | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") end. Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) @@ -340,18 +345,18 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) | Op.Ascaled scale offset, r1::nil => if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) - else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") + else error (Errors.msg "Htlgen: translate_arr_access address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) then ret (Vvari stack (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4)))) (boplitz Vmul r2 (scale / 4)))) - else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") + else error (Errors.msg "Htlgen: translate_arr_access address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") + else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset") + | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing") end. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 7909688..b70e11c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -320,14 +320,14 @@ Lemma translate_instr_tr_op : translate_instr op args s = OK e s' i -> tr_op op args e. Proof. - intros. +(* intros. destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *; try (match goal with [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] => repeat (destruct args; try discriminate) end); monadInv H; constructor. -Qed. +Qed.*) Admitted. (* FIXME: Currently admitted because added Osel *) Hint Resolve translate_instr_tr_op : htlspec. Ltac unfold_match H := diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 700b8e3..a0f3ab3 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -58,7 +58,8 @@ let pprint_binop l r = | Vor -> unsigned "|" | Vxor -> unsigned "^" | Vshl -> unsigned "<<" - | Vshr -> unsigned ">>" + | Vshr -> signed ">>>" + | Vshru -> unsigned ">>" let unop = function | Vneg -> " ~ " diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b4b2f00..b80678e 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -130,7 +130,8 @@ Inductive binop : Type := | Vor : binop (** or (binary [|]) *) | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) -| Vshr : binop. (** shift right ([>>]) *) +| Vshr : binop (** shift right ([>>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) (** ** Unary Operators *) @@ -305,6 +306,7 @@ Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> | Vxor => vxor | Vshl => vshl | Vshr => vshr + | Vshru => vshr (* FIXME: should not be the same operation. *) end. Definition unop_run (op : unop) : value -> value := -- cgit From 11ff840afe29c5340582e513613dc70c13879997 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 20 Jun 2020 10:18:25 +0100 Subject: Add proof of nat equiv --- src/verilog/Value.v | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index b1ee353..18a69ef 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,7 +19,7 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. (* end hide *) @@ -335,7 +335,7 @@ Proof. rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. split. apply Zle_0_pos. - assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt. + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. Qed. @@ -366,3 +366,16 @@ Lemma boolToValue_ValueToBool : forall b, valueToBool (boolToValue 32 b) = b. Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. + +Lemma ZToValue_valueToNat : + forall x sz, + (x < 2^(Z.of_nat sz))%Z -> + valueToNat (ZToValue sz x) = Z.to_nat x. +Proof. + destruct x; intros; unfold ZToValue, valueToNat; simpl. + - rewrite wzero'_def. apply wordToNat_wzero. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. auto. + inversion H. destruct (2 ^ Z.of_nat sz)%Z eqn:?; try discriminate. + Set Printing All. + Search positive Z. + - lia. -- cgit From 7370b2a56b9e2c72f3afca0f256b8d18a00f7143 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 20 Jun 2020 10:46:28 +0100 Subject: Add bugs to support more operations --- src/translation/HTLgen.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 11580cd..4fcb557 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -260,7 +260,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") end. -(** Translate an instruction to a statement. *) +(** Translate an instruction to a statement. FIX mulhs mulhu *) Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := match op, args with | Op.Omove, r::nil => ret (Vvar r) @@ -269,8 +269,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhs") - | Op.Omulhu, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhu") + | Op.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) @@ -291,7 +291,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n)))) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + | Op.Ororimm n, r::nil => ret (Vbinop Vand (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Oshldimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshldimm") | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => -- cgit From cffce3f73e270b2b1d2d94181d7665763b2f965a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 20 Jun 2020 10:59:34 +0100 Subject: Some fixes, but still buggy probably --- src/translation/HTLgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 4fcb557..935f9a1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -291,8 +291,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n)))) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (Vbinop Vand (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) - | Op.Oshldimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshldimm") + | Op.Ororimm n, r::nil => ret (Vbinop Vor (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n))) + | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => do tc <- translate_condition c rl; -- cgit From c02c4c9c4f1e4529526676e5e6aca2b44dd4584c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 09:47:18 +0100 Subject: Add print for debug always block in module --- src/verilog/PrintVerilog.ml | 23 ++++++++++++++++++----- src/verilog/PrintVerilog.mli | 2 +- 2 files changed, 19 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index a0f3ab3..2d8af02 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -175,12 +175,25 @@ let testbench = "module testbench; endmodule " -let pprint_module i n m = +let debug_always i clk state = concat [ + indent i; "reg [31:0] count;\n"; + indent i; "initial count = 0;\n"; + indent i; "always @(posedge " ^ register clk ^ ") begin\n"; + indent (i+1); "if(count[0:0] == 10'd0) begin\n"; + indent (i+2); "$display(\"Cycle count %d\", count);\n"; + indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n"; + indent (i+1); "end\n"; + indent (i+1); "count <= count + 1;\n"; + indent i; "end\n" + ] + +let pprint_module debug i n m = let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in let outputs = [m.mod_finish; m.mod_return] in concat [ indent i; "module "; (extern_atom n); "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; fold_map (pprint_module_item (i+1)) m.mod_body; + if debug then debug_always i m.mod_clk m.mod_st else ""; indent i; "endmodule\n\n" ] @@ -195,11 +208,11 @@ let print_result pp lst = let print_value pp v = fprintf pp "%s" (literal v) -let print_globdef pp (id, gd) = +let print_globdef debug pp (id, gd) = match gd with - | Gfun(Internal f) -> pstr pp (pprint_module 0 id f) + | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f) | _ -> () -let print_program pp prog = - List.iter (print_globdef pp) prog.prog_defs; +let print_program debug pp prog = + List.iter (print_globdef debug pp) prog.prog_defs; pstr pp testbench diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 0df9d06..6544e52 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -18,6 +18,6 @@ val print_value : out_channel -> Value.value -> unit -val print_program : out_channel -> Verilog.program -> unit +val print_program : bool -> out_channel -> Verilog.program -> unit val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit -- cgit From 9089af0dbd8dc079c16501c73727df82c34c530d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 09:58:18 +0100 Subject: Only print out main as everything is inlined --- src/verilog/PrintVerilog.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 2d8af02..5dc0386 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -188,14 +188,16 @@ let debug_always i clk state = concat [ ] let pprint_module debug i n m = - let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in - let outputs = [m.mod_finish; m.mod_return] in - concat [ indent i; "module "; (extern_atom n); - "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; - fold_map (pprint_module_item (i+1)) m.mod_body; - if debug then debug_always i m.mod_clk m.mod_st else ""; - indent i; "endmodule\n\n" - ] + if (extern_atom n) = "main" then + let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in + let outputs = [m.mod_finish; m.mod_return] in + concat [ indent i; "module "; (extern_atom n); + "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; + fold_map (pprint_module_item (i+1)) m.mod_body; + if debug then debug_always i m.mod_clk m.mod_st else ""; + indent i; "endmodule\n\n" + ] + else "" let print_result pp lst = let rec print_result_in pp = function -- cgit From f38fbe6e56bdf69cb5892b5397366ec3d0db9073 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 12:15:53 +0100 Subject: Admit everything temporarily --- src/translation/HTLgen.v | 51 ++++++++++++++++++++++++++++++++++++++++++- src/translation/HTLgenproof.v | 10 ++++----- src/translation/HTLgenspec.v | 6 ++--- 3 files changed, 58 insertions(+), 9 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 935f9a1..f109a8e 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -199,6 +199,41 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := | _, _ => Error (Errors.msg "HTL.add_instr") end. +Lemma add_node_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_node_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))) + (add_node_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. @@ -359,6 +394,18 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing") end. +Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := + match ns with + | n :: ns' => (i, n) :: enumerate (i+1) ns' + | nil => nil + end. + +Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := + List.map (fun a => match a with + (i, n) => (Vlit (natToValue 32 i), Vnonblock (Vvar st) (Vlit (posToValue 32 n))) + end) + (enumerate 0 ns). + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -381,7 +428,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Icond cond args n1 n2 => do e <- translate_condition cond args; add_branch_instr e n n1 n2 - | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented") + | Ijumptable r tbl => + do s <- get; + add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) | Ireturn r => match r with | Some r' => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 4b7f268..9786d23 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -205,7 +205,7 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. +(* Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. Lemma symbols_preserved: @@ -574,16 +574,16 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. - Hint Resolve transl_final_states : htlproof. + Hint Resolve transl_final_states : htlproof.*) Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. - eapply Smallstep.forward_simulation_plus. +(* eapply Smallstep.forward_simulation_plus. apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. - exact transl_step_correct. -Qed. + exact transl_step_correct.*) +Admitted. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index b70e11c..887a696 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -370,7 +370,7 @@ Lemma iter_expand_instr_spec : c!pc = Some instr -> tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). Proof. - induction l; simpl; intros; try contradiction. +(* induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). - subst. @@ -428,8 +428,8 @@ Proof. - eapply IHl. apply EQ0. assumption. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. -Qed. + destruct H2. inv H2. contradiction. assumption. assumption.*) +Admitted. Hint Resolve iter_expand_instr_spec : htlspec. Theorem transl_module_correct : -- cgit From 3ec28d050aebc305c6df5b4b95bcf91498ff11cc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 17:53:54 +0100 Subject: Admit the value proof --- src/verilog/Value.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index ad946ca..253595b 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -381,6 +381,8 @@ Proof. - rewrite wzero'_def. apply wordToNat_wzero. - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. auto. inversion H. destruct (2 ^ Z.of_nat sz)%Z eqn:?; try discriminate. - Set Printing All. - Search positive Z. - - lia. +(* Set Printing All. + Search positive Z.*) + admit. + - admit. +Admitted. -- cgit From 8c48e9e1094f037835698c88782772c8b3250a76 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 23 Jun 2020 11:34:16 +0100 Subject: More to proof --- src/verilog/Value.v | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 253595b..bde98b8 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -374,15 +374,17 @@ Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. Lemma ZToValue_valueToNat : forall x sz, + sz > 0 -> (x < 2^(Z.of_nat sz))%Z -> valueToNat (ZToValue sz x) = Z.to_nat x. Proof. destruct x; intros; unfold ZToValue, valueToNat; simpl. - rewrite wzero'_def. apply wordToNat_wzero. - - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. auto. - inversion H. destruct (2 ^ Z.of_nat sz)%Z eqn:?; try discriminate. -(* Set Printing All. - Search positive Z.*) - admit. - - admit. -Admitted. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. + unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. + rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. + Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) + Search Pos.to_nat. + (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) + Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). + econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. -- cgit From 624f1ee6ed054db89abc0c0a8bb58566119fadae Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 Jun 2020 10:45:16 +0100 Subject: Fix assumption of main --- src/translation/HTLgen.v | 22 +++++++----- src/translation/HTLgenproof.v | 77 ++++++++++++++++++++++++++++++---------- src/translation/HTLgenspec.v | 81 +++++++++++++------------------------------ 3 files changed, 97 insertions(+), 83 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index f109a8e..0482c61 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -283,7 +283,6 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) - | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) | Op.Ascaled scale offset, r1::nil => ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) | Op.Aindexed2scaled scale offset, r1::r2::nil => @@ -529,7 +528,7 @@ Definition transl_module (f : function) : Errors.res module := Definition transl_fundef := transf_partial_fundef transl_module. -Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. +(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) (*Definition transl_main_fundef f : Errors.res HTL.fundef := match f with @@ -546,11 +545,18 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -(*Definition main_is_internal (p : RTL.program): Prop := +Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := let ge := Globalenvs.Genv.globalenv p in - forall b m, - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m). + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. -Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }. -*) +Definition transl_program (p : RTL.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9786d23..c40b737 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -87,12 +87,23 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + main_is_internal p = true. + +Definition match_prog_matches : + forall p tp, + match_prog p tp -> + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Proof. intros. unfold match_prog in H. tauto. Qed. Lemma transf_program_match: forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. Proof. - intros. apply Linking.match_transform_partial_program; auto. + intros. unfold transl_program in H. + destruct (main_is_internal p) eqn:?; try discriminate. + unfold match_prog. split. + apply Linking.match_transform_partial_program; auto. + assumption. Qed. Lemma regs_lessdef_add_greater : @@ -205,13 +216,16 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. -(* Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Lemma TRANSL' : + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Proof. intros; apply match_prog_matches; assumption. Qed. + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. - Proof - (Genv.find_symbol_transf_partial TRANSL). + Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. Lemma function_ptr_translated: forall (b: Values.block) (f: RTL.fundef), @@ -219,7 +233,7 @@ Section CORRECTNESS. exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -229,21 +243,21 @@ Section CORRECTNESS. exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. Proof. - intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof - (Genv.senv_transf_partial TRANSL). + (Genv.senv_transf_partial TRANSL'). Hint Resolve senv_preserved : htlproof. Lemma eval_correct : - forall sp op rs args m v v' e asr asa f, + forall sp op rs args m v v' e asr asa f s s' i, Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> - tr_op op args e -> + translate_instr op args s = OK e s' i -> val_value_lessdef v v' -> Verilog.expr_runp f asr asa e v'. Admitted. @@ -441,6 +455,7 @@ Section CORRECTNESS. assumption. + - admit. - (* Return *) econstructor. split. eapply Smallstep.plus_two. @@ -540,6 +555,17 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_step_correct : htlproof. + Lemma main_tprog_internal : + forall b f, + Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> + Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). + Admitted. + + Lemma option_inv : + forall A x y, + @Some A x = Some y -> x = y. + Proof. intros. inversion H. trivial. Qed. + (* Had to admit proof because currently there is no way to force main to be Internal. *) Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), @@ -548,20 +574,33 @@ Section CORRECTNESS. Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. Proof. induction 1. + destruct TRANSL. unfold main_is_internal in H4. + repeat (unfold_match H4). + assert (f = AST.Internal f1). apply option_inv. + rewrite <- Heqo0. rewrite <- H1. replace b with b0. + auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. exploit function_ptr_translated; eauto. intros [tf [A B]]. unfold transl_fundef, Errors.bind in B. + unfold AST.transf_partial_fundef, Errors.bind in B. repeat (unfold_match B). inversion B. subst. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial TRANSL); eauto. + apply (Genv.init_mem_transf_partial TRANSL'); eauto. replace (AST.prog_main tprog) with (AST.prog_main prog). rewrite symbols_preserved; eauto. symmetry; eapply Linking.match_program_main; eauto. - Admitted. - (*eexact A. trivial. + apply main_tprog_internal. replace ge0 with ge in * by auto. + replace b0 with b in *. rewrite symbols_preserved. + replace (AST.prog_main tprog) with (AST.prog_main prog). + assumption. + symmetry; eapply Linking.match_program_main; eauto. + apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. + constructor. - apply transl_module_correct. auto. - Qed.*) + apply transl_module_correct. eassumption. + Qed. Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : @@ -574,16 +613,16 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. - Hint Resolve transl_final_states : htlproof.*) + Hint Resolve transl_final_states : htlproof. Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. -(* eapply Smallstep.forward_simulation_plus. + eapply Smallstep.forward_simulation_plus. apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. - exact transl_step_correct.*) -Admitted. + exact transl_step_correct. +Qed. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 887a696..d0d16ba 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -113,41 +113,13 @@ Ltac monadInv H := statemachine that is created by the translation contains the correct translations for each of the elements *) -Inductive tr_op : Op.operation -> list reg -> expr -> Prop := -| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r) -| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n)) -| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r)) -| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2) -| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2) -| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n) -| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2) -| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2) -| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2) -| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2) -| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2) -| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n) -| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2) -| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n) -| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2) -| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n) -| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r)) -| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2) -| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n) -| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2) -| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n) -| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e -| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e -| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e -| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r). -Hint Constructors tr_op : htlspec. - Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : forall n, tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) | tr_instr_Iop : - forall n op args e dst, - tr_op op args e -> + forall n op args dst s s' e i, + translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, @@ -168,7 +140,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c src n, translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src)) - (state_goto st n). + (state_goto st n) +| tr_instr_Ijumptable : + forall cexpr tbl r, + cexpr = tbl_to_case_expr st tbl -> + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) @@ -315,21 +291,6 @@ Ltac rewrite_states := remember (?x ?s) as c1; remember (?x ?s') as c2; try subst end. -Lemma translate_instr_tr_op : - forall op args s s' e i, - translate_instr op args s = OK e s' i -> - tr_op op args e. -Proof. -(* intros. - destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *; - try (match goal with - [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] => - repeat (destruct args; try discriminate) - end); - monadInv H; constructor. -Qed.*) Admitted. (* FIXME: Currently admitted because added Osel *) -Hint Resolve translate_instr_tr_op : htlspec. - Ltac unfold_match H := match type of H with | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate @@ -343,7 +304,7 @@ Ltac inv_add_instr' H := end; repeat unfold_match H; inversion H. Ltac inv_add_instr := - match goal with + lazymatch goal with | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -356,6 +317,10 @@ Ltac inv_add_instr := inv_add_instr' H | H: context[add_branch_instr _ _ _ _] |- _ => monadInv H; inv_incr; inv_add_instr + | H: context[add_node_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_node_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr end. Ltac destruct_optional := @@ -370,7 +335,7 @@ Lemma iter_expand_instr_spec : c!pc = Some instr -> tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). Proof. -(* induction l; simpl; intros; try contradiction. + induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). - subst. @@ -383,15 +348,13 @@ Proof. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST. - constructor. eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H14. contradiction. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence. - rewrite HST. econstructor. apply EQ1. - eapply in_map with (f := fst) in H14. contradiction. + + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. @@ -409,6 +372,12 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. + * inversion H14. constructor. congruence. + * apply in_map with (f := fst) in H14. contradiction. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. @@ -428,8 +397,8 @@ Proof. - eapply IHl. apply EQ0. assumption. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption.*) -Admitted. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. Hint Resolve iter_expand_instr_spec : htlspec. Theorem transl_module_correct : -- cgit