diff options
author | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
commit | 7971f2f570de84204aeca2cb72001dc3e824501d (patch) | |
tree | da10753bc6563944309bd23b4dff41185a3e9e43 /src | |
parent | 6426456c4cc7c6d11cf0204ff3d3c0aa18762323 (diff) | |
parent | 86e1d027bb556e0e1f5a39c93b41130603f4f9ad (diff) | |
download | vericert-kvx-7971f2f570de84204aeca2cb72001dc3e824501d.tar.gz vericert-kvx-7971f2f570de84204aeca2cb72001dc3e824501d.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src')
-rw-r--r-- | src/translation/HTLgenproof.v | 123 | ||||
-rw-r--r-- | src/verilog/AssocMap.v | 19 | ||||
-rw-r--r-- | src/verilog/HTL.v | 61 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 9 |
4 files changed, 156 insertions, 56 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index e719070..204451c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -21,7 +21,7 @@ From compcert Require Import Globalenvs. From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. From coqup Require HTL Verilog. -Import AssocMapNotation. +Local Open Scope assocmap. Hint Resolve Smallstep.forward_simulation_plus : htlproof. Hint Resolve AssocMap.gss : htlproof. @@ -37,25 +37,40 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := - forall st assoc, - s = HTL.State m st assoc -> + forall st assoc res, + s = HTL.State res m st assoc -> assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st). Hint Unfold state_st_wf : htlproof. +Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop := +| match_stacks_nil : + match_stacks nil nil +| match_stacks_cons : + forall cs lr r f sp pc rs m assoc + (TF : tr_module f m) + (ST: match_stacks cs lr) + (MA: match_assocmaps f rs assoc), + match_stacks (RTL.Stackframe r f sp pc rs :: cs) + (HTL.Stackframe r m pc assoc :: lr). + Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st +| match_state : forall assoc sf f sp rs mem m st res (MASSOC : match_assocmaps f rs assoc) (TF : tr_module f m) - (WF : state_st_wf m (HTL.State m st assoc)), + (WF : state_st_wf m (HTL.State res m st assoc)) + (MS : match_stacks sf res), match_states (RTL.State sf f sp st rs mem) - (HTL.State m st assoc) -| match_returnstate : forall v v' stack m, - val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v m) (HTL.Returnstate v') + (HTL.State res m st assoc) +| match_returnstate : + forall + v v' stack m res + (MS : match_stacks stack res), + val_value_lessdef v v' -> + match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v') | match_initial_call : - forall f m m0 st + forall f m m0 (TF : tr_module f m), - match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap). + match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := @@ -156,6 +171,20 @@ Ltac unfold_func H := | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) end. +Lemma init_reg_assoc_empty : + forall f l, + match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). +Proof. + induction l; simpl; constructor; intros. + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. +Qed. + Section CORRECTNESS. Variable prog : RTL.program. @@ -234,10 +263,10 @@ Section CORRECTNESS. *) Definition transl_instr_prop (instr : RTL.instruction) : Prop := - forall m assoc fin rtrn st stmt trans, + forall m assoc fin rtrn st stmt trans res, tr_instr fin rtrn st instr stmt trans -> exists assoc', - HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). + HTL.step tge (HTL.State res m st assoc) Events.E0 (HTL.State res m st assoc'). Theorem transl_step_correct: forall (S1 : RTL.state) t S2, @@ -329,7 +358,7 @@ Section CORRECTNESS. (* match_states *) assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. rewrite <- H1. - constructor. apply rs0. + constructor. unfold_merge. apply regs_lessdef_add_match. constructor. @@ -343,6 +372,7 @@ Section CORRECTNESS. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + assumption. - econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -367,7 +397,7 @@ Section CORRECTNESS. destruct b. rewrite assumption_32bit. - apply match_state. apply rs0. + apply match_state. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. @@ -375,8 +405,9 @@ Section CORRECTNESS. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. apply AssocMap.gss. + assumption. rewrite assumption_32bit. - apply match_state. apply rs0. + apply match_state. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. @@ -384,6 +415,7 @@ Section CORRECTNESS. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. apply AssocMap.gss. + assumption. - (* Return *) econstructor. split. @@ -400,7 +432,7 @@ Section CORRECTNESS. trivial. rewrite AssocMap.gso. rewrite AssocMap.gso. - unfold state_st_wf in WF. apply WF. trivial. + unfold state_st_wf in WF. eapply WF. trivial. apply st_greater_than_res. apply st_greater_than_res. trivial. apply HTL.step_finish. @@ -410,10 +442,10 @@ Section CORRECTNESS. apply finish_not_return. apply AssocMap.gss. rewrite Events.E0_left. trivial. - - constructor. constructor. - - destruct (assoc!r) eqn:?. - inversion H11. subst. + constructor. + assumption. + constructor. + - inversion H11. subst. econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. @@ -422,14 +454,11 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. econstructor; simpl; trivial. - apply Verilog.erun_Vvar. - rewrite AssocMap.gso. - apply Heqo. apply not_eq_sym. apply finish_not_res. + apply Verilog.erun_Vvar. trivial. unfold_merge. - trivial. rewrite AssocMap.gso. rewrite AssocMap.gso. - unfold state_st_wf in WF. apply WF. trivial. + unfold state_st_wf in WF. eapply WF. trivial. apply st_greater_than_res. apply st_greater_than_res. trivial. apply HTL.step_finish. @@ -440,8 +469,38 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. trivial. - constructor. simpl. - Admitted. + constructor. assumption. simpl. inversion MASSOC. subst. + unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. + apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. + apply st_greater_than_res. + + - inversion MSTATE; subst. inversion TF; subst. + econstructor. split. apply Smallstep.plus_one. + eapply HTL.step_call. + + constructor. apply regs_lessdef_add_greater. + apply greater_than_max_func. + apply init_reg_assoc_empty. assumption. unfold state_st_wf. + intros. inv H1. apply AssocMap.gss. constructor. + - inversion MSTATE; subst. inversion MS; subst. econstructor. + split. apply Smallstep.plus_one. + constructor. + + constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto. + apply regs_lessdef_add_greater. apply greater_than_max_func. auto. + + unfold state_st_wf. intros. inv H. rewrite AssocMap.gso. + rewrite AssocMap.gss. trivial. apply st_greater_than_res. + + Unshelve. + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (ZToValue 32 0). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + Qed. Hint Resolve transl_step_correct : htlproof. Lemma transl_initial_states : @@ -467,12 +526,14 @@ Section CORRECTNESS. Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : - forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog)) + forall (s1 : Smallstep.state (RTL.semantics prog)) + (s2 : Smallstep.state (HTL.semantics tprog)) (r : Integers.Int.int), match_states s1 s2 -> - Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. + Smallstep.final_state (RTL.semantics prog) s1 r -> + Smallstep.final_state (HTL.semantics tprog) s2 r. Proof. - intros. inv H0. inv H. inv H4. constructor. trivial. + intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. Hint Resolve transl_final_states : htlproof. diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 88b13a6..5d531d5 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -202,9 +202,16 @@ Ltac unfold_merge := unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); rewrite AssocMapExt.merge_base_1. -Module AssocMapNotation. - Notation "a ! b" := (AssocMap.get b a) (at level 1). - Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). - Notation "a # b" := (find_assocmap 32 b a) (at level 1). - Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). -End AssocMapNotation. +Declare Scope assocmap. +Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. +Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. +Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. +Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. +Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. + +Local Open Scope assocmap. +Lemma find_get_assocmap : + forall assoc r v, + assoc ! r = Some v -> + assoc # r = v. +Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index cb081b2..2e4ef1a 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -30,6 +30,8 @@ hardware-like layout that is still similar to the register transfer language instantiations and that we now describe a state machine instead of a control-flow graph. *) +Local Open Scope assocmap. + Definition reg := positive. Definition node := positive. @@ -52,22 +54,42 @@ Definition fundef := AST.fundef module. Definition program := AST.program fundef unit. +Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl') + | _, _ => empty_assocmap + end. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (assoc : assocmap), + stackframe. + Inductive state : Type := | State : - forall (m : module) + forall (stack : list stackframe) + (m : module) (st : node) (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), - state -| Returnstate : forall v : value, state. + (arr_assoc : AssocMap.t (list value)), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g t m st ctrl data + forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 @@ -91,27 +113,40 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asa' = AssocMapExt.merge (list value) nasa2 basa2 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> - step g (State m st asr asa) t (State m pstval asr' asa') + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : - forall g t m st asr asa retval, + forall g m st asr asa retval sf, asr!(m.(mod_finish)) = Some (1'h"1") -> asr!(m.(mod_return)) = Some retval -> - step g (State m st asr asa) t (Returnstate retval). + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g m args res, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) + (init_regs args m.(mod_params))) + (AssocMap.empty (list value))) +| step_return : + forall g m asr i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) + (AssocMap.empty (list value))). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b m0 st m, + | initial_state_intro: forall b m0 m, let ge := Globalenvs.Genv.globalenv p in Globalenvs.Genv.init_mem p = Some m0 -> Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> - st = m.(mod_entrypoint) -> - initial_state p (State m st empty_assocmap (AssocMap.empty (list value))). + initial_state p (Callstate nil m nil). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, retvali = valueToInt retval -> - final_state (Returnstate retval) retvali. + final_state (Returnstate nil retval) retvali. Definition semantics (m : program) := - Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 74c08fe..845d706 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -32,7 +32,8 @@ From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. Import HexNotationValue. -Import AssocMapNotation. + +Local Open Scope assocmap. Set Implicit Arguments. @@ -291,17 +292,13 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack (Vlit v) v | erun_Vvar : forall fext reg stack v r, - reg!r = Some v -> + reg#r = v -> expr_runp fext reg stack (Vvar r) v | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> arr_assocmap_lookup stack r (valueToNat i) = Some v -> expr_runp fext reg stack (Vvari r iexp) v - | erun_Vvar_empty : - forall fext reg stack r sz, - reg!r = None -> - expr_runp fext reg stack (Vvar r) (ZToValue sz 0) | erun_Vinputvar : forall fext reg stack r v, fext!r = Some v -> |