diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 7 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 21 | ||||
| -rw-r--r-- | src/test/power.sail | 4 | ||||
| -rw-r--r-- | src/test/run_power.ml | 2 |
4 files changed, 26 insertions, 8 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index bbcec75b..0bba3b7e 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -2214,6 +2214,13 @@ let rec resume mode stack value = | Action action stack -> Action action (Hole_frame id exp t_level env mem stack) | Error l s -> Error l s end + | (Hole_frame id exp t_level env mem stack, Nothing) -> + match resume mode stack Nothing with + | Value v -> + match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end + | Action action stack -> Action action (Hole_frame id exp t_level env mem stack) + | Error l s -> Error l s + end | (Thunk_frame exp t_level env mem Top,_) -> match interp_main mode t_level env mem exp with | (o,_,_) -> o end | (Thunk_frame exp t_level env mem stack,value) -> diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index ba501577..908b008f 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -19,15 +19,17 @@ let to_bits l = (List.map (fun b -> match b with let from_bits l = (List.map (fun b -> match b with | Interp.V_lit (L_aux L_zero _) -> false | _ -> true end) l) -let rec to_bytes l = match l with +let rec to_bytes l = match (List.reverse l) with | [] -> [] | (a::b::c::d::e::f::g::h::rest) -> - (natFromInteger(integerFromBoolList (true,[a;b;c;d;e;f;g;h])))::(to_bytes rest) + (natFromInteger(integerFromBoolList (false,[a;b;c;d;e;f;g;h])))::(to_bytes rest) end let intern_value v = match v with | Bitvector bs -> Interp.V_vector 0 true (to_bits bs) - | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))) + | Bytevector bys -> Interp.V_vector 0 true + (to_bits (List.reverse + (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))) | Unknown -> Interp.V_unknown end @@ -40,11 +42,11 @@ end let extern_value mode for_mem v = match v with | Interp.V_vector _ true bits -> if for_mem - then (Bytevector (to_bytes (from_bits bits)), Nothing) + then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing) else (Bitvector (from_bits bits), Nothing) | Interp.V_track (Interp.V_vector _ true bits) regs -> if for_mem - then (Bytevector (to_bytes (from_bits bits)), + then (Bytevector (List.reverse (to_bytes (from_bits bits))), if (mode.Interp.track_values) then (Just (List.map (fun r -> extern_reg r Nothing) regs)) else Nothing) @@ -72,13 +74,20 @@ type mem_function = (string * Should probably be expanded into a parameter to mode as with above *) let memory_functions = - [ ("MEM", (Just(Read_plain), Just(Write_plain), + [ ("MEMr", (Just(Read_plain), Nothing, (fun mode v -> match v with | Interp.V_tuple [location;length] -> match length with | Interp.V_lit (L_aux (L_num len) _) -> let (v,regs) = extern_value mode true location in (v,len,regs) end end))); + ("MEMw", (Nothing, Just(Write_plain), + (fun mode v -> match v with + | Interp.V_tuple [location;length] -> + match length with + | Interp.V_lit (L_aux (L_num len) _) -> + let (v,regs) = extern_value mode true location in + (v,len,regs) end end))); ] let rec interp_to_outcome mode thunk = diff --git a/src/test/power.sail b/src/test/power.sail index 5f1f532b..9a89c9e4 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -333,8 +333,8 @@ register (bit[64]) NIA (* next instruction address *) register (bit[64]) CIA (* current instruction address *) -val extern forall Nat 'n. ( nat , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw -val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr (* XXX effect for trap? *) val extern unit -> unit effect pure trap diff --git a/src/test/run_power.ml b/src/test/run_power.ml index 667792c0..70cf5d4b 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -33,7 +33,9 @@ let mem = ref Mem.empty ;; let add_mem byte addr = assert(byte >= 0 && byte < 256); + (*Printf.printf "adder is %s, byte is %s\n" (Big_int.string_of_big_int addr) (string_of_int byte);*) let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in + (*Printf.printf "adder is %s byte is %s\n" (val_to_string addr) (string_of_int byte);*) match addr with | Bytevector addr -> mem := Mem.add addr byte !mem ;; |