diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 14 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 2 | ||||
| -rw-r--r-- | src/test/run_power.ml | 9 |
3 files changed, 15 insertions, 10 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index b59b4144..4dea7217 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -20,17 +20,21 @@ 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 (List.reverse l) with +let rec to_bytes l = match l with | [] -> [] | (a::b::c::d::e::f::g::h::rest) -> - (natFromInteger(integerFromBoolList (false,[a;b;c;d;e;f;g;h])))::(to_bytes rest) + (natFromInteger(integerFromBoolList (false,(List.reverse([a;b;c;d;e;f;g;h])))))::(to_bytes rest) end let intern_value v = match v with | Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs) | 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)))) + (List.concat (List.map (fun by -> + match Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num 8) Interp_ast.Unknown); + Interp.V_lit(L_aux (L_num (integerFromNat by)) Interp_ast.Unknown)])) + with + | Interp.V_vector _ _ bits -> bits + | _ -> [] end) bys)) | Unknown -> Interp.V_unknown | _ -> Interp.V_unknown end @@ -50,7 +54,7 @@ let rec extern_value mode for_mem v = match v with else Nothing) | Interp.V_vector fst inc bits -> if for_mem - then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing) + then (Bytevector (to_bytes (from_bits bits)), Nothing) else (Bitvector (from_bits bits) inc fst, Nothing) | Interp.V_lit (L_aux L_zero _) -> if for_mem diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index a90dffc2..28d0d862 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -143,7 +143,7 @@ let rec perform_action ((reg, mem) as env) = function if eq_big_int length zero_big_int then [] else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in - (Some (Bytevector((List.rev (reading location length)))), env) + (Some (Bytevector(reading location length)), env) | Write_mem0(_,(Bytevector location), length, _, (Bytevector bytes),_,_) -> let rec writing location length bytes mem = if eq_big_int length zero_big_int diff --git a/src/test/run_power.ml b/src/test/run_power.ml index 335dde47..83f6549c 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -39,11 +39,12 @@ let reg = ref (Reg.add "dummy" Unknown0 Reg.empty) ;; let add_mem byte addr = assert(byte >= 0 && byte < 256); - Printf.printf "adder is %s, byte is %s\n" (string_of_big_int addr) (string_of_int byte); + (*Printf.printf "adder is %s, byte is %s\n" (string_of_big_int addr) (string_of_int byte);*) let addr = big_int_to_vec true addr (big_int_of_int 64) in - Printf.printf "adder is %s byte is %s\n" (Printing_functions.val_to_string addr) (string_of_int byte); + (*Printf.printf "adder is %s byte is %s\n" (Printing_functions.val_to_string addr) (string_of_int byte);*) match addr with - | Bytevector addr -> mem := Mem.add addr byte !mem + | Bytevector addr -> (*List.iter (fun i -> Printf.printf "%i " i) addr; Printf.printf "\n";*) + mem := Mem.add addr byte !mem ;; let add_section s = @@ -297,7 +298,7 @@ let run () = mainaddr := "0x" ^ (List.fold_left (^) "" (List.map (Printf.sprintf "%02x") addr)); end in Printf.printf "start address: %s\n" !mainaddr; - Printf.printf "%s\n" (Printing_functions.val_to_string (Bytevector !startaddr)); +(* Printf.printf "%s\n" (Printing_functions.val_to_string (Bytevector !startaddr));*) let my_reg = init_reg () in reg := my_reg; (* entry point: unit -> unit fde *) |