diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 14 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 2 |
2 files changed, 10 insertions, 6 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 |