summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-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
4 files changed, 38 insertions, 27 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 02:31:26 +0000