diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 29 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 |
2 files changed, 25 insertions, 8 deletions
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) |