summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem19
-rw-r--r--src/lem_interp/run_interp.ml7
-rw-r--r--src/test/run_power.ml9
3 files changed, 14 insertions, 21 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index b80c3fe7..ceefe421 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -27,20 +27,21 @@ let bool_to_bit b = match b with
| true -> V_lit (L_aux L_one Unknown)
end ;;
-(* XXX always interpret as positive ? *)
-let to_num_dec (V_vector idx false l) =
- V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
+(* BitSeq expects LSB first.
+ * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
+ * hence MSB first.
+ * http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num_inc (V_vector idx true l) =
+ V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
+let to_num_dec (V_vector idx false l) =
V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;
-(* XXX not quite sure about list reversal here - what is the convention for
- * V_vector? cf. above too *)
-let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
- let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
- V_vector 0 false (map bool_to_bit (reverse l)) ;;
let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
- V_vector 0 true (map bool_to_bit l) ;;
+ V_vector 0 true (map bool_to_bit (reverse l)) ;;
+let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
+ let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
+ V_vector 0 false (map bool_to_bit l) ;;
let rec add (V_tuple args) = match args with
(* vector case *)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 0ed3edaa..19daeeb9 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -46,7 +46,7 @@ let rec val_to_string = function
let repr = String.concat "; " (List.map val_to_string l) in
sprintf "list [%s]" repr
| V_vector (first_index, inc, l) ->
- let order = if inc then "little-endian" else "big-endian" in
+ let order = if inc then "big-endian" else "little-endian" in
let repr =
try bitvec_to_string l
with Failure _ -> String.concat "; " (List.map val_to_string l) in
@@ -145,7 +145,6 @@ let perform_action ((reg, mem) as env) = function
| Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) ->
V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) value mem)
(* multi-byte accesses to memory *)
- (* XXX this doesn't deal with endianess at all *)
| Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], sub) ->
let rec fetch k acc =
if eq_big_int k size then slice acc sub else
@@ -153,9 +152,7 @@ let perform_action ((reg, mem) as env) = function
fetch (succ_big_int k) (vconcat acc slice)
in
fetch zero_big_int (V_vector (zero_big_int, true, [])), env
- (* XXX no support for multi-byte slice write at the moment - not hard to add,
- * but we need a function basic read/write first since slice access involves
- * read, fupdate, write. *)
+ (* XXX no support for multi-byte slice write at the moment *)
| Write_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, V_vector (m, inc, vs)) ->
(* normalize input vector so that it is indexed from 0 - for slices *)
let value = V_vector (zero_big_int, inc, vs) in
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index e8f47d64..91bb0448 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -14,19 +14,14 @@ let rec foldli f acc ?(i=0) = function
| x::xs -> foldli f (f i acc x) ~i:(i+1) xs
;;
-let little_endian = false ;;
+let big_endian = true ;;
let hex_to_big_int s = Big_int.big_int_of_int64 (Int64.of_string s) ;;
-(* XXX POWER is big-endian - cheating until we have Kathy's switch *)
-let flip_vec (V_vector (i, inc, l)) = V_vector (i, not inc, l)
-
let big_int_to_vec b size =
- flip_vec (
- (if little_endian then to_vec_inc else to_vec_dec)
+ (if big_endian then to_vec_inc else to_vec_dec)
size
(V_lit (L_aux (L_num b, Unknown)))
- )
;;
let mem = ref Mem.empty ;;