6 files changed, 26 insertions, 5 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a3bd294a..b1a23a5e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -215,6 +215,7 @@ type action =
  | Read_mem of id * value * maybe (nat * nat)
  | Write_mem of id * value * maybe (nat * nat) * value
  | Barrier of id * value
+ | Footprint of id * value
  | Write_next_IA of value (* Perhaps not needed? *)
  | Nondet of list (exp tannot)
  | Call_extern of string * value
@@ -1830,6 +1831,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
           then 
             (Action (Barrier (id_of_string name_ext) v)
                     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
+	  else if has_depend_effect effects
+	  then 
+	    (Action (Footprint (id_of_string name_ext) v)
+	            (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
 	  else if has_wmem_effect effects
 	  then 
 	    let (wv,v) =
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 4a9964e2..2af90d6f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -456,6 +456,8 @@ let rec interp_to_outcome mode context thunk =
 	| Just barrier -> 
 	  Barrier barrier (IState next_state context)
 	| _ -> Error ("Barrier " ^ i ^ " function not found") end
+    | Interp.Footprint (Id_aux (Id i) _) lval ->
+      Footprint (IState next_state context)
     | Interp.Nondet exps -> 
       let nondet_states = List.map (Interp.set_in_context next_state) exps in
       Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context)
@@ -540,6 +542,8 @@ let rec ie_loop mode register_values (IState interp_state context) =
       (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true))
     | Barrier barrier_k i_state ->
       (E_barrier barrier_k)::(ie_loop mode register_values i_state)
+    | Footprint i_state ->
+      E_footprint::(ie_loop mode register_values i_state)
     | Internal _ _ next -> (ie_loop mode register_values next)
      end ;;
   
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 830877e1..2699fc38 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -272,6 +272,8 @@ type outcome =
 | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
+(* Tell the system to dynamically recalculate dependency footprint *)
+| Footprint of instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
 | Read_reg of reg_name * (register_value -> instruction_state) 
 (* Request to write register *)
@@ -289,6 +291,7 @@ type event =
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
+| E_footprint 
 | E_read_reg of reg_name
 | E_write_reg of reg_name * register_value
 | E_escape
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 2790aee7..d83341c8 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -10,6 +10,11 @@ open import Bool
 
 type signed = Unsigned | Signed
 
+let rec power (a: integer) (b: integer) : integer =
+ if b <= 0 
+ then 1
+ else a * (power a (b-1))
+
 let hardware_mod (a: integer) (b:integer) : integer = 
  if a < 0 && b < 0
  then (abs a) mod (abs b)
@@ -638,6 +643,7 @@ let library_functions direction = [
   ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1);
   ("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1);
+  ("power", arith_op power);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index e87600a3..dab33767 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -17,18 +17,18 @@ let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
 val lit_eq: lit -> lit -> bool
 let lit_eq (L_aux left _) (L_aux right _) =
    match (left, right) with
-   | (L_unit, L_unit) -> true
    | (L_zero, L_zero) -> true
    | (L_one, L_one) -> true
-   | (L_true, L_true) -> true
-   | (L_false, L_false) -> true
+   | (L_bin b, L_bin b') -> b = b'
+   | (L_hex h, L_hex h') -> h = h'
    | (L_zero, L_num i) -> i = 0
    | (L_num i,L_zero) -> i = 0
    | (L_one, L_num i) -> i = 1
    | (L_num i, L_one) -> i = 1
    | (L_num n, L_num m) -> n = m
-   | (L_hex h, L_hex h') -> h = h'
-   | (L_bin b, L_bin b') -> b = b'
+   | (L_unit, L_unit) -> true
+   | (L_true, L_true) -> true
+   | (L_false, L_false) -> true
    | (L_undef, L_undef) -> true
    | (L_string s, L_string s') -> s = s'
    | (_, _) -> false
@@ -50,6 +50,7 @@ end
 val has_rmem_effect : list base_effect -> bool
 val has_barr_effect : list base_effect -> bool
 val has_wmem_effect : list base_effect -> bool
+val has_depend_effect : list base_effect -> bool
 let rec has_effect which efcts =
   match efcts with
   | [] -> false
@@ -69,6 +70,7 @@ let rec has_effect which efcts =
 let has_rmem_effect = has_effect BE_rmem
 let has_barr_effect = has_effect BE_barr
 let has_wmem_effect = has_effect BE_wmem
+let has_depend_effect = has_effect BE_depend
 
 let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
 let get_effects (Typ_aux t _) =
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index ca4abe17..76f216ee 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -82,6 +82,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
   | BE_barr -> "barr"
+  | BE_depend -> "depend"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")