From b71b75aa7f9e4db0575b01cf25b7ad6dd88abff4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 4 Jun 2020 20:03:10 +0100 Subject: Finished main proof with small assumptions --- src/verilog/AssocMap.v | 19 +++++++++++----- src/verilog/HTL.v | 60 +++++++++++++++++++++++++++++++++++++++----------- src/verilog/Verilog.v | 9 +++----- 3 files changed, 63 insertions(+), 25 deletions(-) (limited to 'src/verilog') 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 bf38b29..82378b3 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. @@ -51,21 +53,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) - (assoc : assocmap), - state -| Returnstate : forall v : value, state. + (assoc : assocmap), 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 assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval, + forall g m st ctrl data assoc0 assoc1 assoc2 + assoc3 nbassoc0 nbassoc1 f stval pstval sf, m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -79,27 +102,38 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := assoc3 = merge_assocmap nbassoc1 assoc2 -> assoc3!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> - step g (State m st assoc0) t (State m pstval assoc3) + step g (State sf m st assoc0) Events.E0 (State sf m pstval assoc3) | step_finish : - forall g t m st assoc retval, + forall g m st assoc retval sf, assoc!(m.(mod_finish)) = Some (1'h"1") -> assoc!(m.(mod_return)) = Some retval -> - step g (State m st assoc) t (Returnstate retval). + step g (State sf m st assoc) 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)))) +| step_return : + forall g m assoc i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc assoc :: sf) i) Events.E0 + (State sf m pc ((assoc # mst <- (posToValue 32 pc)) # r <- i)). 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). + 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 ce7ddd9..cccdf9a 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. Definition reg : Type := positive. Definition node : Type := positive. @@ -246,12 +247,8 @@ Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := expr_runp fext assoc (Vlit v) v | erun_Vvar : forall fext assoc v r, - assoc!r = Some v -> + assoc#r = v -> expr_runp fext assoc (Vvar r) v - | erun_Vvar_empty : - forall fext assoc r sz, - assoc!r = None -> - expr_runp fext assoc (Vvar r) (ZToValue sz 0) | erun_Vinputvar : forall fext assoc r v, fext!r = Some v -> -- cgit