Make interpreter able to read registers during translate address and decode.

This is not yet connected to any model and not yet tested.

Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).

6 files changed, 66 insertions, 48 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 9ed4efed..df17fffd 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -251,6 +251,32 @@ let update_reg_value_slice reg_name v start stop v2 =
     else
       (Interp.fupdate_vector_slice v_internal v2_internal start stop))
 
+(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
+(*TODO immediate: this will be impacted by need to change slicing *)
+let rec find_reg_name reg = function
+  | [] -> Nothing
+  | (reg_name,v)::registers ->
+    match (reg,reg_name) with
+      | (Reg i start size dir, Reg n start2 size2 dir2) -> 
+        if i = n && size = size2 then (Just v) else find_reg_name reg registers
+      | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) -> 
+        if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+      | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> 
+        if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+      | (Reg_slice  i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) ->
+        if i=n 
+        then if p1=p3 && p2 = p4 then (Just v)
+             else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2))
+             else find_reg_name reg registers
+          else find_reg_name reg registers
+      | (Reg_field i _ _ f _,Reg_field n _ _ fn _) ->
+        if i=n && f = fn then (Just v) else find_reg_name reg registers
+      | (Reg_f_slice i _ _ f _ (p1,p2), Reg_f_slice n _ _ fn _ (p3,p4)) ->
+        if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers
+      | _ -> find_reg_name reg registers
+end end
+
+
 let initial_instruction_state top_level main args = 
   let e_args = match args with
     | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
@@ -262,7 +288,7 @@ let initial_instruction_state top_level main args =
 
 type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal
 
-let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
+let rec interp_to_value_helper arg ivh_mode err_str instr direction registers thunk =
   let errk_str = match ivh_mode with
     | Ivh_translate -> "translate"
     | Ivh_decode -> "decode"
@@ -291,7 +317,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
       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 ivh_mode err_str instr direction 
+          interp_to_value_helper arg ivh_mode err_str instr direction registers
             (fun _ -> Interp.resume (make_interpreter_mode true false) stack (Just (f value)))
       end 
     | (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) ->
@@ -304,12 +330,24 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction thunk =
             | _ -> (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 slice) stack,_,_) ->
       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
         | _ -> Assert_extra.failwith "Reg not following expected structure" end in
-      (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)))
+      let err_value =
+        (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)))
+      in
+      (match registers with
+        | Nothing -> err_value
+        | Just(regs) ->
+          let reg = extern_reg r slice in
+          match find_reg_name reg regs with
+            | Nothing -> err_value
+            | Just v ->
+              let value = intern_reg_value v in
+              interp_to_value_helper arg ivh_mode err_str instr direction registers
+                (fun _ -> Interp.resume (make_interpreter_mode true false) stack (Just value)) end end)      
     | (Interp.Action (Interp.Write_reg _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error ("Register write request in a " ^ errk_str)))
     | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
@@ -338,7 +376,7 @@ let build_context defs reads writes write_eas write_vals barriers externs =
       Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes write_eas write_vals barriers externs end
 
 
-let translate_address top_level end_flag thunk_name address =
+let translate_address top_level end_flag thunk_name registers address =
   let (Address bytes i) = address in
   let mode = make_mode true false end_flag in
   let int_mode = mode.internal_mode in
@@ -348,9 +386,10 @@ let translate_address top_level end_flag thunk_name address =
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   let (address,error) = interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction
-    (fun _ -> Interp.resume 
-      int_mode 
-      (Interp.Thunk_frame 
+      registers
+      (fun _ -> Interp.resume 
+        int_mode 
+        (Interp.Thunk_frame 
          (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown)
                    [arg;E_aux (E_lit (L_aux (L_num 0) Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)])
             (Interp_ast.Unknown, Nothing)) 
@@ -395,14 +434,14 @@ let migrate_typ = function
 end
 
 
-let decode_to_istate top_level value = 
+let decode_to_istate top_level registers value = 
   let mode = make_interpreter_mode true false in
   let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
   let intern_val = intern_opcode direction value in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
-  let (instr_decoded,error) = interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction
+  let (instr_decoded,error) = interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction registers
     (fun _ -> Interp.resume 
       mode 
       (Interp.Thunk_frame 
@@ -431,6 +470,7 @@ let decode_to_istate top_level value =
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
       let (instr_decoded,error) =
         interp_to_value_helper value Ivh_unsupported val_str instr_external internal_direction
+          registers
         (fun _ -> Interp.resume 
          mode
           (Interp.Thunk_frame 
@@ -453,8 +493,8 @@ let decode_to_istate top_level value =
 end
 
 
-let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_decode_error  = 
-  match decode_to_istate top_level value with
+let decode_to_instruction (top_level:context) registers (value:opcode) : instruction_or_decode_error  = 
+  match decode_to_istate top_level registers value with
   | Instr inst is -> IDE_instr inst
   | Decode_error de -> IDE_decode_error de
   end
@@ -609,30 +649,6 @@ let interp mode (IState interp_state context) =
     | (o,_) -> o
 end 
 
-(*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
-(*TODO immediate: this will be impacted by need to change slicing *)
-let rec find_reg_name reg = function
-  | [] -> Nothing
-  | (reg_name,v)::registers ->
-    match (reg,reg_name) with
-      | (Reg i start size dir, Reg n start2 size2 dir2) -> 
-        if i = n && size = size2 then (Just v) else find_reg_name reg registers
-      | (Reg_slice i _ _ (p1,p2), Reg n _ _ _) -> 
-        if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
-      | (Reg_field i _ _ f (p1,p2), Reg n _ _ _) -> 
-        if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
-      | (Reg_slice  i _ _ (p1,p2), Reg_slice n _ _ (p3,p4)) ->
-        if i=n 
-        then if p1=p3 && p2 = p4 then (Just v)
-             else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2))
-             else find_reg_name reg registers
-          else find_reg_name reg registers
-      | (Reg_field i _ _ f _,Reg_field n _ _ fn _) ->
-        if i=n && f = fn then (Just v) else find_reg_name reg registers
-      | (Reg_f_slice i _ _ f _ (p1,p2), Reg_f_slice n _ _ fn _ (p3,p4)) ->
-        if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers
-      | _ -> find_reg_name reg registers
-end end
 
 (*Update slice potentially here*)
 let reg_size = function
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 61074ca0..90b22fd5 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -880,11 +880,11 @@ type i_state_or_error =
 
 
 (** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
-val decode_to_istate : context -> opcode -> i_state_or_error
+val decode_to_istate : context -> maybe (list (reg_name * register_value)) -> opcode -> i_state_or_error
 
 (** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
 (** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
-val decode_to_instruction : context -> opcode -> instruction_or_decode_error
+val decode_to_instruction : context -> maybe (list (reg_name * register_value))-> opcode -> instruction_or_decode_error
 
 (*Function to generate the state to run from an instruction form; is always an Instr*)
 val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*)
@@ -1149,7 +1149,8 @@ let clear_low_order_bits_of_address a =
   | _ -> failwith "Address does not contain 8 bytes"
   end
 
-val translate_address : context -> end_flag -> string -> address -> maybe address * maybe nat
+val translate_address :
+  context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe nat
 
 val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
 let byte_list_of_memory_value endian mv = 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index e40dfe9f..9abf0442 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -340,7 +340,8 @@ let run
           show "exiting current evaluation" "" "" "";
           step e,env', e
         | Escape _ -> assert false
-        | Error0 _ -> assert false
+        | Error0 _ -> failwith "Internal error"
+        | Fail0 _ -> failwith "Assertion in program failed"
         | Done ->
           show "done evalution" "" "" "";
           assert false
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 75ed3b33..5ceff43a 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -906,7 +906,7 @@ let fetch_instruction_opcode_and_update_ia model addr_trans =
     let pc_addr = address_of_register_value nextPC in
     (match pc_addr with
     | Some pc_addr ->
-      let pc_a = match addr_trans pc_addr with
+      let pc_a = match addr_trans None pc_addr with
         | Some a, _ -> integer_of_address a
         | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
         | _ -> failwith "Neither an address or a code on translate address" in
@@ -990,7 +990,7 @@ let run () =
           endian mode, and translate function name 
   *)
   let addr_trans = translate_address context E_big_endian "TranslateAddress" in
-  let startaddr = match addr_trans startaddr_internal with
+  let startaddr = match addr_trans None startaddr_internal with
     | Some a, _ -> integer_of_address a
     | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
     | _ -> failwith "Neither an address or a code on translate address"
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index ff4e5caa..05150f47 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -989,7 +989,7 @@ let fetch_instruction_opcode_and_update_ia model addr_trans =
     let pc_addr = address_of_register_value nextPC in
     (match pc_addr with
     | Some pc_addr ->
-      let pc_a = match addr_trans pc_addr with
+      let pc_a = match addr_trans None pc_addr with
         | Some a, _ -> integer_of_address a
         | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
         | _ -> failwith "Neither an address or a code on translate address" in
@@ -1021,7 +1021,7 @@ let rec fde_loop count context model mode track_dependencies opcode addr_trans =
     interactf "\n**** instruction %d from address %s ****\n"
       count (Printing_functions.register_value_to_string (get_pc_address model));
     if !break_point && count = !break_instr then begin break_point := false; eager_eval := false end;
-    let (instruction,istate) = match Interp_inter_imp.decode_to_istate context opcode with
+    let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
       | Instr(instruction,istate) ->
         interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
         (instruction,istate)
@@ -1073,7 +1073,7 @@ let run () =
           endian mode, and translate function name 
   *)
   let addr_trans = translate_address context E_big_endian "TranslateAddress" in
-  let startaddr = match addr_trans startaddr_internal with
+  let startaddr = match addr_trans None startaddr_internal with
     | Some a, _ -> integer_of_address a
     | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
     | _ -> failwith "Neither an address or a code on translate address"
diff --git a/src/parser.mly b/src/parser.mly
index 8868340d..00bcb465 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -962,7 +962,7 @@ patsexp:
     { peloc (Pat_exp($1,$3)) }
 
 letbind:
-  | Let_ atomic_pat Eq atomic_exp
+  | Let_ atomic_pat Eq exp
     { lbloc (LB_val_implicit($2,$4)) }
   | Let_ typquant atomic_typ atomic_pat Eq exp
     { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
@@ -1256,11 +1256,11 @@ def:
     { dloc (DEF_spec($1)) }
   | default_typ
     { dloc (DEF_default($1)) }
-  | Register atomic_typ id
+  | Register typ id
     { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
   | Register Alias id Eq exp
     { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) }
-  | Register Alias atomic_typ id Eq exp
+  | Register Alias typ id Eq exp
     { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) }
   | Scattered scattered_def
     { dloc (DEF_scattered $2) }