Merge branch 'develop' into arrays-proof

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