From 044a68b1b215125e2651c637f28c794536d27ba5 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 14 Jun 2020 16:41:27 +0100 Subject: Array semantics now uses dependent Array type. --- _CoqProject | 2 +- src/translation/HTLgen.v | 14 +++++------ src/translation/Veriloggen.v | 5 ++-- src/verilog/HTL.v | 21 +++++++--------- src/verilog/Verilog.v | 57 ++++++++++++++++++++++++-------------------- 5 files changed, 50 insertions(+), 49 deletions(-) diff --git a/_CoqProject b/_CoqProject index a1026ed..7965da9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -14,4 +14,4 @@ -R lib/CompCert/flocq compcert.flocq -R lib/CompCert/lib compcert.lib -R lib/CompCert/x86 compcert.x86 --R lib/CompCert/x86_32 compcert.x86_64 +-R lib/CompCert/x86_32 compcert.x86_32 diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index d35a296..1c67fe7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -131,7 +131,7 @@ Lemma declare_reg_state_incr : s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). @@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)) @@ -393,7 +393,7 @@ Lemma create_reg_state_incr: s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) (st_datapath s) (st_controllogic s)). @@ -405,7 +405,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := s.(st_st) (Pos.succ r) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) (st_controllogic s)) @@ -418,7 +418,7 @@ Lemma create_arr_state_incr: (Pos.succ (st_freshreg s)) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. @@ -430,7 +430,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (Pos.succ r) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)) (create_arr_state_incr s sz ln i). @@ -466,7 +466,7 @@ Definition max_state (f: function) : state := mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) - (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st))) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index efe3565..2b9974b 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := match scldecl with - | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' + | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' | nil => nil end. Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := match arrdecl with - | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' + | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' | nil => nil end. @@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := m.(mod_return) m.(mod_st) m.(mod_stk) + m.(mod_stk_len) m.(mod_params) body m.(mod_entrypoint). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index c509248..8149ddf 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,7 +17,7 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value AssocMap. +From coqup Require Import Coquplib Value AssocMap Array. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. @@ -66,13 +66,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. -Fixpoint zeroes' (acc : list value) (n : nat) : list value := - match n with - | O => acc - | S n => zeroes' ((NToValue 32 0)::acc) n - end. - -Definition zeroes : nat -> list value := zeroes' nil. +Definition empty_stack (m : module) : AssocMap.t (Array value) := + (AssocMap.set m.(mod_stk) (Verilog.zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))). (** * Operational Semantics *) @@ -84,7 +79,7 @@ Inductive stackframe : Type := (m : module) (pc : node) (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), + (arr_assoc : AssocMap.t (Array value)), stackframe. Inductive state : Type := @@ -93,7 +88,7 @@ Inductive state : Type := (m : module) (st : node) (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (arr_assoc : AssocMap.t (Array value)), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -114,7 +109,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f (Verilog.mkassociations asr empty_assocmap) - (Verilog.mkassociations asa (AssocMap.empty (list value))) + (Verilog.mkassociations asa (empty_stack m)) ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> @@ -125,7 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> asr' = merge_assocmap nasr2 basr2 -> - asa' = AssocMapExt.merge (list value) nasa2 basa2 -> + asa' = AssocMapExt.merge (Array value) nasa2 basa2 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') @@ -140,7 +135,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value)))) + (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, mst = mod_st m -> diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 8b83d49..3ab3f10 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -27,7 +27,7 @@ From Coq Require Import Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap. +From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. @@ -48,38 +48,31 @@ Record associations (A : Type) : Type := }. Definition reg_associations := associations value. -Definition arr_associations := associations (list value). +Definition arr_associations := associations (Array value). -Definition assocmap_arr := AssocMap.t (list value). +Definition assocmap_arr := AssocMap.t (Array value). Definition merge_associations {A : Type} (assoc : associations A) := mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) (AssocMap.empty A). -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value := +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := match a ! r with - | None => natToValue 32 0 - | Some arr => nth i arr (natToValue 32 0) + | None => None + | Some arr => array_get_error i arr end. -Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := - match i, l with - | _, nil => nil - | S n, h :: t => h :: list_set n x t - | O, h :: t => x :: t - end. - -Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := +Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := match a ! r with | None => a - | Some arr => AssocMap.set r (list_set i v arr) a + | Some arr => a # r <- (array_set i v arr) end. Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). + mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)). + mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). Definition block_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). @@ -87,8 +80,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). -Inductive scl_decl : Type := Scalar (sz : nat). -Inductive arr_decl : Type := Array (sz : nat) (ln : nat). +Inductive scl_decl : Type := VScalar (sz : nat). +Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST @@ -217,6 +210,7 @@ Record module : Type := mkmodule { mod_return : reg; mod_st : reg; (**r Variable that defines the current state, it should be internal. *) mod_stk : reg; + mod_stk_len : nat; mod_args : list reg; mod_body : list module_item; mod_entrypoint : node; @@ -234,7 +228,7 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := AssocMap.t value. +Definition fext := assocmap. Definition fextclk := nat -> fext. (** ** State @@ -272,7 +266,7 @@ Inductive state : Type := (m : module) (st : node) (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (arr_assoc : AssocMap.t (Array value)), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -324,7 +318,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> - arr_assocmap_lookup stack r (valueToNat i) = v -> + arr_assocmap_lookup stack r (valueToNat i) = Some v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vinputvar : forall fext reg stack r v, @@ -690,16 +684,27 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := Definition genv := Globalenvs.Genv.t fundef unit. +Fixpoint list_zeroes' (acc : list value) (n : nat) : list value := + match n with + | O => acc + | S n => list_zeroes' ((NToValue 32 0)::acc) n + end. + +Definition list_zeroes : nat -> list value := list_zeroes' nil. +Definition zeroes (n : nat) : Array value := make_array (list_zeroes n). +Definition empty_stack (m : module) : AssocMap.t (Array value) := + (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))). + Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g, mis_stepp f (mkassociations asr empty_assocmap) - (mkassociations asa (AssocMap.empty (list value))) + (mkassociations asa (empty_stack m)) m.(mod_body) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1)-> asr' = merge_assocmap nasr1 basr1 -> - asa' = AssocMapExt.merge (list value) nasa1 basa1 -> + asa' = AssocMapExt.merge (Array value) nasa1 basa1 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') @@ -714,13 +719,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint)) (init_params args m.(mod_args))) - (AssocMap.empty (list value))) + (empty_stack m)) | 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))). + (empty_stack m)). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := -- cgit