Fix array semantics merge granularity.

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')