summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_inter_imp.lem16
-rw-r--r--src/lem_interp/interp_interface.lem4
-rw-r--r--src/lem_interp/run_interp.ml4
-rw-r--r--src/lem_interp/run_interp_model.ml41
-rw-r--r--src/test/run_power.ml16
5 files changed, 46 insertions, 35 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 908b008f..8265fd5e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -26,8 +26,8 @@ let rec to_bytes l = match (List.reverse l) with
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
+ | Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs)
+ | Bytevector bys inc fst -> Interp.V_vector fst inc
(to_bits (List.reverse
(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
| Unknown -> Interp.V_unknown
@@ -40,17 +40,17 @@ let extern_reg r slice = match (r,slice) with
end
let extern_value mode for_mem v = match v with
- | Interp.V_vector _ true bits ->
+ | Interp.V_vector fst inc bits ->
if for_mem
- 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 ->
+ then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
+ else (Bitvector (from_bits bits) inc fst, Nothing)
+ | Interp.V_track (Interp.V_vector fst inc bits) regs ->
if for_mem
- then (Bytevector (List.reverse (to_bytes (from_bits bits))),
+ then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst,
if (mode.Interp.track_values)
then (Just (List.map (fun r -> extern_reg r Nothing) regs))
else Nothing)
- else (Bitvector (from_bits bits), Nothing)
+ else (Bitvector (from_bits bits) inc fst, Nothing)
| _ -> (Unknown,Nothing)
end
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index e821aae8..684257f6 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -17,12 +17,12 @@ type write_kind = Write_plain | Write_conditional | Write_release
type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
type value =
-| Bitvector of list bool (* For register accesses *)
+| Bitvector of list bool * bool * integer (* For register accesses : in conformance with Sail, tracks order and starting lsb number*)
(*To discuss: ARM8 uses at least one abstract record form for
some special registers, with no clear mapping to bits. Should
we permit Record of (string * Bitvector) values as well?
*)
-| Bytevector of list word8 (* For memory accesses *)
+| Bytevector of list word8 * bool * integer (* For memory accesses : see above *)
| Unknown
(*To add: an abstract value representing an unknown but named memory address?*)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 91930974..37c73d66 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -48,8 +48,8 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
;;
let val_to_string v = match v with
- | Bitvector bools -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
- | Bytevector words ->
+ | Bitvector(bools, _, _) -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
+ | Bytevector(words, _, _)->
"0x" ^ (String.concat ""
(List.map (function
| 10 -> "A"
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index aaff997f..9591b918 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -48,12 +48,13 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
;;
let val_to_string v = match v with
- | Bitvector bools -> let l = List.length bools in
+ | Bitvector(bools, inc, fst)-> let l = List.length bools in
(string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
- | Bytevector words ->
+ | Bytevector(words, inc, fst)->
let l = List.length words in
- (String.concat ""
- (List.map (fun i -> (Printf.sprintf "0x%x " i)) words))
+ (string_of_int l) ^ " bytes --" ^
+ (String.concat ""
+ (List.map (fun i -> (Printf.sprintf "0x%x " i)) words))
| Unknown0 -> "Unknown"
let reg_name_to_string = function
@@ -187,13 +188,19 @@ module Mem = struct
add key valu m
let to_string loc v =
- sprintf "[%s] -> %s" (val_to_string (Bytevector loc)) (string_of_int v)
+ sprintf "[%s] -> %x" (val_to_string (Bytevector(loc, true, zero_big_int))) v
end ;;
let rec slice bitvector (start,stop) =
match bitvector with
- | Bitvector bools -> Bitvector (Interp.from_n_to_n start stop bools)
- | Bytevector bytes -> Bytevector (Interp.from_n_to_n start stop bytes) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
+ | Bitvector(bools, inc, fst) ->
+ Bitvector ((Interp.from_n_to_n (if inc then (sub_big_int start fst) else (sub_big_int fst start))
+ (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bools),
+ inc,
+ (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int)))
+
+ | Bytevector(bytes, inc, fst) ->
+ Bytevector((Interp.from_n_to_n start stop bytes),inc,fst) (*This is wrong, need to explode and re-encode, but maybe never happens?*)
| Unknown0 -> Unknown0
;;
@@ -210,15 +217,19 @@ let rec list_update index start stop e vals =
let bool_to_byte = function | true -> 0 | false -> 1
let bitvector_to_bool = function
- | Bitvector [b] -> b
- | Bytevector [0] -> false
- | Bytevector [1] -> true
+ | Bitvector([b],_,_) -> b
+ | Bytevector([0],_,_) -> false
+ | Bytevector([1],_,_) -> true
;;
let fupdate_slice original e (start,stop) =
match original with
- | Bitvector bools -> Bitvector (list_update zero_big_int start stop e bools)
- | Bytevector bytes -> Bytevector (list_update zero_big_int start stop (bool_to_byte e) bytes) (*Probably also wrong, does this happen?*)
+ | Bitvector(bools,inc,fst) ->
+ Bitvector((list_update zero_big_int
+ (if inc then (sub_big_int start fst) else (sub_big_int fst start))
+ (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) e bools), inc, fst)
+ | Bytevector(bytes,inc,fst) ->
+ Bytevector((list_update zero_big_int start stop (bool_to_byte e) bytes),inc,fst) (*Probably also wrong, does this happen?*)
| Unknown0 -> Unknown0
;;
@@ -249,13 +260,13 @@ let rec perform_action ((reg, mem) as env) = function
let old_val = Reg.find id reg in
let new_val = fupdate_slice old_val (bitvector_to_bool value) (combine_slices range mini_range) in
(None,(Reg.add id new_val reg,mem))
- | Read_mem0(_,Bytevector location, length, _,_) ->
+ | Read_mem0(_,Bytevector(location,_,_), length, _,_) ->
let rec reading location length =
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)
- | Write_mem0(_,Bytevector location, length, _, Bytevector(bytes),_,_) ->
+ (Some (Bytevector((List.rev (reading location length)), true, zero_big_int)), env) (*TODO: how to get order back here? *)
+ | Write_mem0(_,(Bytevector(location,_,_)), length, _, (Bytevector(bytes,_,_)),_,_) ->
let rec writing location length bytes mem =
if eq_big_int length zero_big_int
then mem
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 70cf5d4b..3c58ebfa 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -37,7 +37,7 @@ let add_mem byte addr =
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
+ | Bytevector(addr,_,_) -> mem := Mem.add addr byte !mem
;;
let add_section s =
@@ -68,11 +68,11 @@ let lr_init_value = Big_int.zero_big_int
let init_reg () =
let init name value size =
(* fix index - this is necessary for CR, indexed from 32 *)
-(* let offset = function
- V_vector(_, inc, v) ->
- V_vector(Big_int.big_int_of_int (64 - size), inc, v)
- | _ -> assert false in*)
- name, (*offset*) (big_int_to_vec false value (Big_int.big_int_of_int size)) in
+ let offset = function
+ | Bitvector(bits,inc,fst) ->
+ Bitvector(bits,inc,Big_int.big_int_of_int (64 - size))
+ | _ -> assert false in
+ name, offset (big_int_to_vec false value (Big_int.big_int_of_int size)) in
List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
(* XXX execute main() directly until we can handle the init phase *)
init "CIA" (hex_to_big_int !mainaddr) 64;
@@ -81,7 +81,7 @@ let init_reg () =
init "CTR" Big_int.zero_big_int 64;
init "CR" Big_int.zero_big_int 32;
init "LR" lr_init_value 64;
- "mode64bit", Bitvector [true];
+ "mode64bit", Bitvector([true],true,Big_int.zero_big_int);
]
;;
@@ -109,7 +109,7 @@ let get_reg reg name =
;;
let eq_zero = function
- | Bitvector bools -> List.for_all (not) bools
+ | Bitvector(bools,_,_) -> List.for_all (not) bools
;;
let rec fde_loop count main_func parameters mem reg ?mode prog =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 19:22:31 +0000