Merge branch 'master' of bitbucket.org:Peter_Sewell/l2

1 files changed, 31 insertions, 23 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index ba6e5107..ed576d2d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -14,15 +14,15 @@ val extern_reg_value : reg_name -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
 
-let make_interp_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values|>;;
+let make_interp_mode eager_eval tracking_values = 
+  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;
 
 let make_mode eager_eval tracking_values endian = 
   <|internal_mode = make_interp_mode eager_eval tracking_values;
     endian = endian|>;;
 let tracking_dependencies mode = mode.internal_mode.Interp.track_values
 let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
-let make_default_mode _ = <|internal_mode = <| Interp.eager_eval = false; Interp.track_values = false |>;
-                            endian = E_big_endian|>;;
+let make_default_mode _ = <|internal_mode = make_interp_mode false false; endian = E_big_endian|>;;
 
 let bitl_to_ibit = function 
   | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
@@ -292,41 +292,41 @@ let initial_instruction_state top_level main args =
 
 let rec interp_to_value_helper arg err_str instr direction thunk = 
   match thunk() with
-    | Interp.Value value -> (Just value,Nothing)
-    | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
-    | Interp.Action (Interp.Call_extern i value) stack ->
+    | (Interp.Value value,_,_) -> (Just value,Nothing)
+    | (Interp.Error l msg,_,_) -> (Nothing, Just (Internal_error msg))
+    | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
       match List.lookup i (Interp_lib.library_functions direction) with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
           interp_to_value_helper arg err_str instr direction 
 	    (fun _ -> Interp.resume (make_interp_mode true false) stack (Just (f value)))
       end 
-    | Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack ->
+    | (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) ->
       match e with
 	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
 	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
 	| E_lit (L_aux (L_string str) _) -> (Nothing, Just (Internal_error ("Exit called with message: " ^ str)))
 	| E_id (Id_aux (Id i) _) -> 
 	  (match (Interp.resume (make_interp_mode true false) (Interp.set_in_context stack exp) Nothing) with
-	    | Interp.Value (Interp.V_lit (L_aux (L_string str) _)) ->
+	    | (Interp.Value (Interp.V_lit (L_aux (L_string str) _)),_,_) ->
 	      (Nothing, Just (Internal_error ("Exit called when decoding "^err_str ^" with message: " ^ str)))
 	    | _ -> (Nothing, Just (Internal_error ("Exit called with unrecognized expression bound to an id " ^ i))) end)
 	| _ -> (Nothing, Just (Internal_error "Exit called with unrecognized expression"))
       end 
-    | Interp.Action (Interp.Read_reg r _) _ ->
+    | (Interp.Action (Interp.Read_reg r _) _,_,_) ->
       let rname = match r with 
 	| Interp.Reg (Id_aux (Id i) _) _ _ -> i
 	| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i end in
       (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a decode of " ^ err_str)))
-    | Interp.Action (Interp.Write_reg _ _ _) _ ->
+    | (Interp.Action (Interp.Write_reg _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Register write request in a decode"))
-    | Interp.Action (Interp.Read_mem _ _ _) _ ->
+    | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Read memory request in a decode"))
-    | Interp.Action (Interp.Write_mem _ _ _ _) _ ->
+    | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write memory request in a decode"))
-    | Interp.Action (Interp.Write_ea _ _) _ ->
+    | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write ea request in a decode"))
-    | Interp.Action (Interp.Write_memv _ _) _ ->
+    | (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write memory value request in a decode"))
     | _ -> (Nothing, Just (Internal_error "Non expected action in a decode"))
 end
@@ -389,7 +389,7 @@ let decode_to_istate top_level value =
 		  (name, [(p_name,t, (extern_ifield_value name p_name value t))], effects)
 		| (Interp.V_tuple vals,parms) -> 
 		  (name, 
-		   (Interp.map2 (fun value (p_name,ie_typ) -> 
+		   (Interp_utilities.map2 (fun value (p_name,ie_typ) -> 
 		     let t = migrate_typ ie_typ in
 		     (p_name,t,(extern_ifield_value name p_name value t))) vals parms), effects)
           end end end in 
@@ -451,9 +451,9 @@ let rec interp_to_outcome mode context thunk =
   let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   match thunk () with
-  | Interp.Value _ -> Done
-  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
-  | Interp.Action a next_state ->
+  | (Interp.Value _,lm,le) -> Done
+  | (Interp.Error l msg,lm,le) -> Error msg 
+  | (Interp.Action a next_state,lm,le) ->
     match a with
     | Interp.Read_reg reg_form slice -> 
       Read_reg (extern_reg reg_form slice) 
@@ -526,9 +526,14 @@ let rec interp_to_outcome mode context thunk =
 	| _ -> 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)
+    | Interp.Nondet exps tag ->
+      match tag with
+	| Tag_unknown ->
+	  let possible_states = List.map (Interp.set_in_context next_state) exps in
+	  Analysis_non_det (List.map (fun i -> IState i context) possible_states) (IState next_state context)
+	| _ -> 
+	  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) end
     | Interp.Call_extern i value -> 
       match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
       | Nothing -> Error ("External function not available " ^ i)
@@ -598,9 +603,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
   match interp mode (IState interp_state context) with
     | Done -> []
     | Error msg -> [E_error msg]
-    | Escape Nothing i_state -> E_escape :: (ie_loop mode register_values i_state)
+    | Escape Nothing i_state -> [E_escape]
     (*Do we want to record anything about the escape expression, which may be a function call*)
-    | Escape _ i_state -> E_escape :: (ie_loop mode register_values i_state) 
+    | Escape _ i_state -> [E_escape] 
     | Read_reg reg i_state_fun -> 
       let v =  match register_values with
 	| Nothing -> unknown_reg (reg_size reg)
@@ -624,6 +629,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
     | Footprint i_state ->
       E_footprint::(ie_loop mode register_values i_state)
     | Internal _ _ next -> (ie_loop mode register_values next)
+    | Analysis_non_det possible_states i_state ->
+      (*TODO: need to merge the stores from the stacks/results somehow (so probably need to have a different loop)*)
+      (List.concat (List.map (ie_loop mode register_values) possible_states))++(ie_loop mode register_values i_state)
      end ;;
   
 let interp_exhaustive register_values i_state =