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/verilog | |
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/verilog')
-rw-r--r-- | src/verilog/AssocMap.v | 19 | ||||
-rw-r--r-- | src/verilog/HTL.v | 61 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 9 |
3 files changed, 64 insertions, 25 deletions
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 -> |