diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 13 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 29 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parser.mly | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 5 |
6 files changed, 37 insertions, 19 deletions
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 |