Support for nondeterministic blocks

6 files changed, 57 insertions, 27 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index e9609f52..f1e7a2ac 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -179,24 +179,24 @@ 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 =
+let rec has_effect which efcts =
   match efcts with
   | [] -> false
   | (BE_aux e _)::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
+    match (which,e) with
+    | (BE_rreg,BE_rreg)    -> true 
+    | (BE_wreg,BE_wreg)    -> true 
+    | (BE_rmem,BE_rmem)    -> true 
+    | (BE_wmem,BE_wmem)    -> true 
+    | (BE_barr,BE_barr)    -> true 
+    | (BE_undef,BE_undef)  -> true 
+    | (BE_unspec,BE_unspec) -> true 
+    | (BE_nondet,BE_nondet) -> true 
+    | _ -> has_effect which efcts
     end 
   end
-let has_rmem_effect = has_effect 2
-let has_barr_effect = has_effect 4
+let has_rmem_effect = has_effect BE_rmem
+let has_barr_effect = has_effect BE_barr
 
 let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
 let get_effects (Typ_aux t _) =
@@ -474,6 +474,16 @@ let rec add_answer_to_stack stack v =
   | Thunk_frame e t_level env mem stack -> Thunk_frame e t_level env mem (add_answer_to_stack stack v)
 end
 
+val set_in_context : stack -> exp tannot -> stack
+let rec set_in_context stack e =
+  match stack with
+    | Top -> Top
+    | Hole_frame id oe t_level env mem Top -> Thunk_frame e t_level env mem Top
+    | Thunk_frame oe t_level env mem Top -> Thunk_frame e t_level env mem Top
+    | Hole_frame _ _ _ _ _ s -> set_in_context s e
+    | Thunk_frame _ _ _ _ s -> set_in_context s e
+end
+
 let id_of_string s = (Id_aux (Id s) Unknown)
 
 let rec combine_typs ts =
@@ -1304,7 +1314,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 								    (l,annot)))
 			                          (fun vs -> (V_vector_sparse b len is_inc (map2 (fun i v -> (i,v)) indexes vs) v)) l_env l_mem [] exps)
 	                 (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot)))) end)	  
-    | E_block(exps) -> interp_block mode t_level l_env l_env l_mem l annot exps
+    | E_block exps -> interp_block mode t_level l_env l_env l_mem l annot exps
+    | E_nondet exps ->
+      (Action (Nondet exps) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem, l_env)
     | E_app f args ->
       (match (exp_list mode t_level (fun es -> E_aux (E_app f es) (l,annot)) 
 		               (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index caf6f52b..0bdd3539 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -78,6 +78,9 @@ let rec interp_to_outcome mode thunk =
       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.Nondet exps -> 
+      let nondet_states = List.map (Interp.set_in_context next_state) exps in
+      Nondet_choice nondet_states next_state      
     | Interp.Call_extern i value -> 
       match List.lookup i external_functions with
       | Nothing -> Error ("External function not available " ^ i)
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index d102c1fe..4d8cc82c 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -29,7 +29,7 @@ type outcome =
 | Barrier of barrier_kind * instruction_state
 | Read_reg of reg_name * (value -> instruction_state) 
 | Write_reg of reg_name * value * instruction_state
-| Nondet_choice of list instruction_state
+| Nondet_choice of list instruction_state * instruction_state
 | Internal of instruction_state
 | Done
 | Error of string
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index e3fe1cbc..e845754d 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -75,6 +75,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
+  | BE_barr -> "barr"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")
@@ -314,6 +315,9 @@ let doc_exp, doc_let =
   | E_block exps ->
       let exps_doc = separate_map (semi ^^ hardline) exp exps in
       surround 2 1 lbrace exps_doc rbrace
+  | E_nondet exps ->
+    let exps_doc = separate_map (semi ^^ hardline) exp exps in
+    string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
   | E_id id -> doc_id id
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) ->
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index b199c09b..f297b5bb 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -90,6 +90,7 @@ let rec compact_exp (E_aux (e, l)) =
   let wrap e = E_aux (e, l) in
   match e with
  | E_block (e :: _) -> compact_exp e
+ | E_nondet (e :: _) -> compact_exp e
  | E_if (e, _, _) ->
      wrap(E_if(compact_exp e, ldots, E_aux(E_block [], tunk)))
  | E_for (i, e1, e2, e3, o, e4) ->
@@ -119,7 +120,7 @@ let rec compact_exp (E_aux (e, l)) =
  | E_field (e, id) ->
      wrap(E_field(compact_exp e, id))
  | E_assign (lexp, e) -> wrap(E_assign(lexp, compact_exp e))
- | E_block [] | E_cast (_, _) | E_internal_cast (_, _)
+ | E_block [] | E_nondet [] | E_cast (_, _) | E_internal_cast (_, _)
  | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ ->
      wrap e
 
@@ -244,7 +245,7 @@ let rec perform_action ((reg, mem) as env) = function
      perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
  (* extern functions *)
  | Call_extern (name, arg) -> eval_external name arg, env
- | Debug l -> unit_lit, env
+ | Debug _ | Nondet _ -> unit_lit, env
  | _ -> assert false
 ;;
 
@@ -337,33 +338,41 @@ let run
       let show act lhs arrow rhs = debugf "%s: %s: %s %s %s\n"
         (grey loc) (green act) lhs (blue arrow) rhs in
       let left = "<-" and right = "->" in
-      let mode' = begin match a with
+      let mode',env' = begin match a with
       | Read_reg (reg, sub) ->
           show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string return);
-          step ()
+          step (),env'
       | Write_reg (reg, sub, value) ->
           assert (return = unit_lit);
           show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string value);
-          step ()
+          step (),env'
       | Read_mem (id, args, sub) ->
           show "read_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) right (val_to_string return);
-          step ()
+          step (),env'
       | Write_mem (id, args, sub, value) ->
           assert (return = unit_lit);
           show "write_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) left (val_to_string value);
-          step ()
+          step (),env'
       (* distinguish single argument for pretty-printing *)
       | Call_extern (f, (V_tuple _ as args)) ->
           show "call_lib" (f ^ val_to_string args) right (val_to_string return);
-          step ()
+          step (),env'
       | Call_extern (f, arg) ->
           show "call_lib" (sprintf "%s(%s)" f (val_to_string arg)) right (val_to_string return);
-          step ()
+          step (),env'
       | Debug _ ->
           assert (return = unit_lit);
           show "breakpoint" "" "" "";
-          step ~force:true ()
-      | Barrier (_, _) | Write_next_IA _ | Nondet _ ->
+          step ~force:true (),env'
+      | Nondet exps ->
+	let stacks = List.sort (fun (_,i1) (_,i2) -> compare i1 i2)
+	                       (List.combine (List.map (set_in_context s) exps)
+	                                     (List.map (fun _ -> Random.bits ()) exps)) in
+	show "nondeterministic evaluation begun" "" "" "";
+	let (_,_,env') = List.fold_right (fun (stack,_) (_,_,env') -> loop mode env' (resume {eager_eval = (mode = Run)} stack None)) stacks (false,mode,env'); in
+	show "nondeterministic evaluation ended" "" "" "";
+	step (),env'
+      | Barrier (_, _) | Write_next_IA _  ->
           failwith "unexpected action"
       end in
       loop mode' env' (resume {eager_eval = (mode' = Run)} s (Some return))
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 0544c573..deb4d4bf 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -798,7 +798,9 @@ let doc_exp, doc_let =
   | E_block exps ->
       let exps_doc = separate_map (semi ^^ hardline) exp exps in
       surround 2 1 lbrace exps_doc rbrace
-(* XXX Need to add E_nondet, not sure how to put the nondet in front of the block *)
+  | E_nondet exps ->
+    let exps_doc = separate_map (semi ^^ hardline) exp exps in
+    string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
   | E_id id -> doc_id id
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))