Add support for memory barrier

11 files changed, 43 insertions, 20 deletions

diff --git a/language/l2.lem b/language/l2.lem
index b19639bb..af6b1485 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -66,6 +66,7 @@ type base_effect_aux =  (* effect *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
+ | BE_barr (* memory barrier *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2.ml b/language/l2.ml
index 76b27874..e46014dc 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -63,6 +63,7 @@ base_effect_aux =  (* effect *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
+ | BE_barr (* memory barrier *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2.ott b/language/l2.ott
index 5d1994e2..c56a186b 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -117,7 +117,7 @@ id :: '' ::=
   | unit			 :: M :: unit {{ ichlo (Id "unit") }}
   | nat				 :: M :: nat  {{ ichlo (Id "nat") }}
   | string                       :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }}
-  | enum                         :: M :: enum {{ ichlo (Id "enum") }}
+  | range                        :: M :: range {{ ichlo (Id "range") }}
   | vector			 :: M :: vector {{ ichlo (Id "vector") }}
   | list			 :: M :: list {{ ichlo (Id "list") }}
   | set                          :: M :: set {{ ichlo (Id "set") }}
@@ -184,6 +184,7 @@ base_effect :: 'BE_' ::=
   | wreg                                :: :: wreg {{ com write register }}
   | rmem                                :: :: rmem {{ com read memory }}
   | wmem                                :: :: wmem {{ com write memory }}
+  | barr                                :: :: barr {{ com memory barrier }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 3146ad2b..b54491bc 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -46,6 +46,7 @@ base_effect_aux =  (* effect *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
+ | BE_barr (* memory barrier *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 03c50d08..e62e4587 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -155,6 +155,7 @@ base_effect :: 'BE_' ::=
   | wreg                                :: :: wreg {{ com write register }}
   | rmem                                :: :: rmem {{ com read memory }}
   | wmem                                :: :: wmem {{ com write memory }}
+  | barr                                :: :: barr {{ com memory barrier }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4d08e9eb..c6c08c67 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -186,13 +186,14 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                              (fun efct -> match efct with
                              | Parse_ast.BE_aux(e,l) ->
                                BE_aux((match e with 
-                               | Parse_ast.BE_rreg -> BE_rreg
-                               | Parse_ast.BE_wreg -> BE_wreg
-                               | Parse_ast.BE_rmem -> BE_rmem
-                               | Parse_ast.BE_wmem -> BE_wmem
+                               | Parse_ast.BE_barr  -> BE_barr
+                               | Parse_ast.BE_rreg  -> BE_rreg
+                               | Parse_ast.BE_wreg  -> BE_wreg
+                               | Parse_ast.BE_rmem  -> BE_rmem
+                               | Parse_ast.BE_wmem  -> BE_wmem
                                | Parse_ast.BE_undef -> BE_undef
-                               | Parse_ast.BE_unspec -> BE_unspec
-                               | Parse_ast.BE_nondet -> BE_nondet),l))
+                               | Parse_ast.BE_unspec-> BE_unspec
+                               | Parse_ast.BE_nondet-> BE_nondet),l))
                              effects)
                | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index f9a64da1..e9609f52 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -175,17 +175,28 @@ let rec to_registers (Defs defs) =
     end 
   end
 
-val has_memory_effect : list base_effect -> bool
-let rec has_memory_effect efcts =
+val has_rmem_effect : list base_effect -> bool
+val has_barr_effect : list base_effect -> bool
+
+(*General has_effect function that selects which effect searched for based on a numeric selector *)
+let rec has_effect (n : nat) efcts =
   match efcts with
   | [] -> false
   | (BE_aux e _)::efcts ->
-    match e with
-    | BE_wreg -> true
-    | BE_wmem -> true
-    | _ -> has_memory_effect efcts
+    match (n,e) with
+    | (0,BE_rreg)   -> true (* read register *)
+    | (1,BE_wreg)   -> true (* write register *)
+    | (2,BE_rmem)   -> true (* read memory *)
+    | (3,BE_wmem)   -> true (* write memory *)
+    | (4,BE_barr)   -> true (* memory barrier *)
+    | (5,BE_undef)  -> true (* undefined-instruction exception *)
+    | (6,BE_unspec) -> true (* unspecified values *)
+    | (7,BE_nondet) -> true (* nondeterminism from intra-instruction parallelism *)
+    | _ -> has_effect n efcts
     end 
   end
+let has_rmem_effect = has_effect 2
+let has_barr_effect = has_effect 4
 
 let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
 let get_effects (Typ_aux t _) =
@@ -1357,10 +1368,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
            end)
         | Tag_extern opt_name ->
           let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
-          if has_memory_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) 
+          if has_rmem_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) 
           then
             (Action (Read_mem (id_of_string name_ext) v Nothing) 
 	            (Hole_frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
+          else if has_barr_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end)
+          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
             (Action (Call_extern name_ext v) 
 	            (Hole_frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 1eb16d9d..caf6f52b 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -75,7 +75,9 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i memory_functions with
       | (Just (_,Just write_k,f)) -> Write_mem write_k (f loc_val) (extern_value true write_val) (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
-      end
+      end 
+    | Interp.Barrier (Id_aux (Id i) _) lval ->
+      Barrier Interp.Barrier_plain next_state (* TODO set up some barrier functions and see if the value would be anything needed *)
     | Interp.Call_extern i value -> 
       match List.lookup i external_functions with
       | Nothing -> Error ("External function not available " ^ i)
diff --git a/src/lexer.mll b/src/lexer.mll
index ad6ea0d9..206df359 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -108,6 +108,7 @@ let kw_table =
      ("quot",			 (fun x -> Quot));
      ("rem",			 (fun x -> Rem));
 
+     ("barr",                    (fun x -> Barr));
      ("rreg",                    (fun x -> Rreg));
      ("wreg",                    (fun x -> Wreg));
      ("rmem",                    (fun x -> Rmem));
diff --git a/src/parser.mly b/src/parser.mly
index 2679c2ca..0ee7093d 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -124,7 +124,7 @@ let make_vector_sugar typ typ1 =
 
 %token And As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End Enumerate Else Extern
 %token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
-%token Rreg Wreg Rmem Wmem Undef Unspec Nondet
+%token Barr Rreg Wreg Rmem Wmem Undef Unspec Nondet
 %token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -282,6 +282,8 @@ kind:
     { K_aux(K_kind($1), loc ()) }
 
 effect:
+  | Barr
+    { efl BE_barr }
   | Rreg 
     { efl BE_rreg }
   | Wreg
diff --git a/src/type_check.ml b/src/type_check.ml
index bb588fc5..739cb6d6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -19,10 +19,7 @@ let get_e_typ (E_aux(_,(_,a))) =
   | Base((_,t),_,_,_) -> t
   | _ -> new_t ()
 
-let typ_error l msg  =
-  raise (Reporting_basic.err_typ 
-           l
-           (msg ))
+let typ_error l msg  = raise (Reporting_basic.err_typ l msg)
 
 let rec field_equivs fields fmaps = 
   match fields with