From dfea5f0f6307177a9127ce29db496a819dcdb232 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 17 Jun 2020 19:53:43 +0100 Subject: Fix array semantics merge granularity. --- src/common/Coquplib.v | 7 +++++++ src/verilog/Array.v | 38 ++++++++++++++++++++++++++++++++++ src/verilog/HTL.v | 16 +++++++-------- src/verilog/Verilog.v | 56 +++++++++++++++++++++++++++++++-------------------- 4 files changed, 87 insertions(+), 30 deletions(-) diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index fd0987b..675ad23 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -47,6 +47,7 @@ Ltac clear_obvious := repeat match goal with | [ H : ex _ |- _ ] => invert H | [ H : ?C _ = ?C _ |- _ ] => invert H + | [ H : _ /\ _ |- _ ] => invert H end. Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. @@ -81,6 +82,12 @@ Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := | _ => None end. +Definition join {A : Type} (a : option (option A)) : option A := + match a with + | None => None + | Some a' => a' + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/verilog/Array.v b/src/verilog/Array.v index 8673f0c..16f5406 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -121,3 +121,41 @@ Proof. unfold array_get. info_eauto with array. Qed. + +Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := + match n with + | O => acc + | S n => list_repeat' (a::acc) a n + end. + +Lemma list_repeat'_len : forall {A : Type} (a : A) n l, + Datatypes.length (list_repeat' l a n) = (n + Datatypes.length l)%nat. +Proof. + induction n; intros; simplify; try reflexivity. + + specialize (IHn (a :: l)). + rewrite IHn. + simplify. + lia. +Qed. + +Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil. + +Lemma list_repeat_len {A : Type} : forall n (a : A), Datatypes.length (list_repeat a n) = n. +Proof. + intros. + unfold list_repeat. + rewrite list_repeat'_len. + simplify. lia. +Qed. + +Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). + +Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := + match x, y with + | a :: t, b :: t' => f a b :: list_combine f t t' + | _, _ => nil + end. + +Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := + make_array (list_combine f x.(arr_contents) y.(arr_contents)). diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 8149ddf..0bf5072 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -66,8 +66,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. -Definition empty_stack (m : module) : AssocMap.t (Array value) := - (AssocMap.set m.(mod_stk) (Verilog.zeroes m.(mod_stk_len)) (AssocMap.empty (Array value))). +Definition empty_stack (m : module) : Verilog.assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). (** * Operational Semantics *) @@ -78,8 +78,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (Array value)), + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), stackframe. Inductive state : Type := @@ -87,8 +87,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (Array value)), state + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -119,8 +119,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> - asr' = merge_assocmap nasr2 basr2 -> - asa' = AssocMapExt.merge (Array value) nasa2 basa2 -> + asr' = Verilog.merge_regs nasr2 basr2 -> + asa' = Verilog.merge_arrs 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') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 3ab3f10..d20ffcd 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -25,6 +25,8 @@ From Coq Require Import Lists.List Program. +Require Import Lia. + Import ListNotations. From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array. @@ -47,25 +49,44 @@ Record associations (A : Type) : Type := assoc_nonblocking : AssocMap.t A }. +Definition arr := (Array (option value)). + Definition reg_associations := associations value. -Definition arr_associations := associations (Array value). +Definition arr_associations := associations arr. + +Definition assocmap_reg := AssocMap.t value. +Definition assocmap_arr := AssocMap.t arr. -Definition assocmap_arr := AssocMap.t (Array value). +Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := + AssocMapExt.merge value new old. -Definition merge_associations {A : Type} (assoc : associations A) := - mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) - (AssocMap.empty A). +Definition merge_cell (new : option value) (old : option value) : option value := + match new, old with + | Some _, _ => new + | _, _ => old + end. + +Definition merge_arr (new : option arr) (old : option arr) : option arr := + match new, old with + | Some new', Some old' => Some (combine merge_cell new' old') + | Some new', None => Some new' + | None, Some old' => Some old' + | None, None => None + end. + +Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := + AssocMap.combine merge_arr new old. Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := match a ! r with | None => None - | Some arr => array_get_error i arr + | Some arr => Option.join (array_get_error i arr) end. Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := match a ! r with | None => a - | Some arr => a # r <- (array_set i v arr) + | Some arr => a # r <- (array_set i (Some v) arr) end. Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := @@ -265,8 +286,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (Array value)), state + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -683,17 +704,8 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := end. 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))). +Definition empty_stack (m : module) : assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : @@ -703,8 +715,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := m.(mod_body) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1)-> - asr' = merge_assocmap nasr1 basr1 -> - asa' = AssocMapExt.merge (Array value) nasa1 basa1 -> + asr' = merge_regs nasr1 basr1 -> + asa' = merge_arrs 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') -- cgit