summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem27
-rw-r--r--src/lem_interp/interp_lib.lem22
-rw-r--r--src/lem_interp/run_interp.ml6
3 files changed, 36 insertions, 19 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index e2d6b781..0a112962 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -263,8 +263,8 @@ let is_lit_vector (L_aux l _) =
end
(* XXX Both make an endian assumption, and should use a flag to switch*)
-val litV_to_vec : lit -> value
-let litV_to_vec (L_aux lit l) =
+val litV_to_vec : lit -> bool -> value
+let litV_to_vec (L_aux lit l) is_inc =
match lit with
| L_hex s ->
let to_v b = V_lit (L_aux b l) in
@@ -295,10 +295,14 @@ let litV_to_vec (L_aux lit l) =
| #'e' -> [L_one ;L_one ;L_one ;L_zero]
| #'f' -> [L_one ;L_one ;L_one ;L_one ] end)
(String.toCharList s))) in
- V_vector 0 true hexes
+ if is_inc
+ then V_vector 0 true hexes
+ else V_vector (integerFromNat ((List.length hexes) -1)) false hexes
| L_bin s ->
let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) (String.toCharList s) in
- V_vector 0 true bits
+ if is_inc
+ then V_vector 0 true bits
+ else V_vector (integerFromNat ((List.length bits) -1)) false bits
end
(* Like List_extra.nth with a integer instead of nat index -
@@ -660,11 +664,11 @@ let rec match_pattern (P_aux p _) value =
match p with
| P_lit(lit) ->
if is_lit_vector lit then
- let (V_vector n inc bits) = litV_to_vec lit in
+ let (V_vector n inc bits) = litV_to_vec lit true in (*TODO use type annotation to select between increasing and decreasing*)
match value with
| V_lit litv ->
if is_lit_vector litv then
- let (V_vector n' inc' bits') = litV_to_vec litv in
+ let (V_vector n' inc' bits') = litV_to_vec litv true in (*TODO find a way to determine increasing or decreasing *)
if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, [])
else (false,false,[])
else (false,false,[])
@@ -918,7 +922,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
match exp with
| E_lit lit ->
if is_lit_vector lit
- then (Value (litV_to_vec lit) Tag_empty,l_mem,l_env)
+ then
+ let is_inc = (match typ with | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
+ (Value (litV_to_vec lit is_inc) Tag_empty,l_mem,l_env)
else (Value (V_lit lit) Tag_empty, l_mem,l_env)
| E_cast ((Typ_aux typ _) as ctyp) exp ->
resolve_outcome (interp_main mode t_level l_env l_mem exp)
@@ -1306,7 +1312,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| E_tuple(exps) ->
exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
- exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
+ let is_inc = (match typ with
+ | T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
+ | _ -> false end) in
+ let base = integerFromNat (if is_inc then 0 else (List.length exps) - 1) in
+ exp_list mode t_level
+ (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base is_inc vals) l_env l_mem [] exps
| E_vector_indexed iexps (Def_val_aux default dannot) ->
let (indexes,exps) = List.unzip iexps in
let (is_inc,base,len) = (match typ with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index a03fad5c..199d070a 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -78,17 +78,23 @@ let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
* http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num signed (V_vector idx inc l) =
(* Word library in Lem expects bitseq with LSB first *)
- let l = if inc then reverse l else l in
+(*TODO: Kathy think more
+ We thought a reverse was needed due to above comments only in inc case.
+ However, we seem to be interpresting bit vectors such that reverse is always needed
+ and despite numbering MSB is on the left.
+*)
+ let l = (*if inc then reverse l else l*) reverse l in
(* Make sure the last bit is a zero to force unsigned numbers *)
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
+(*TODO As with above, consider the reverse here in both cases, where we're again always interpreting with the MSB on the left *)
let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
- V_vector 0 false (map bool_to_bit l) ;;
+ V_vector (len - 1) false (map bool_to_bit (reverse l)) ;;
let to_vec ord len n =
if ord
then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
@@ -131,12 +137,12 @@ let arith_op_vec_range op (V_tuple args) = match args with
end ;;
let arith_op_range_vec_range op (V_tuple args) = match args with
- | [n;(V_vector _ _ _ as l2)] ->
- arith_op op (V_tuple [n;(to_num true l2)])
+ | [n;(V_vector _ ord _ as l2)] ->
+ arith_op op (V_tuple [n;(to_num ord l2)])
end ;;
let arith_op_vec_range_range op (V_tuple args) = match args with
- | [(V_vector _ _ _ as l1);n] ->
- arith_op op (V_tuple [(to_num true l1);n])
+ | [(V_vector _ ord _ as l1);n] ->
+ arith_op op (V_tuple [(to_num ord l1);n])
end ;;
let compare_op op (V_tuple args) = match args with
@@ -155,8 +161,8 @@ let rec vec_concat (V_tuple args) = match args with
| [V_vector n d l; V_vector n' d' l'] ->
(* XXX d = d' ? droping n' ? *)
V_vector n d (l ++ l')
- | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
- | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
+ | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l true; x]) (*TODO, get the correct order*)
+ | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l true]) (*TODO, get the correct order*)
end ;;
let function_map = [
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 91a81634..2f8c5e97 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -62,7 +62,7 @@ let rec val_to_string = function
| V_vector (first_index, inc, l) ->
let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index in
let repr =
- try bitvec_to_string (if inc then l else List.rev l)
+ try bitvec_to_string (* (if inc then l else List.rev l)*) l
with Failure _ ->
sprintf "[%s]" (String.concat "; " (List.map val_to_string l)) in
sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
@@ -148,9 +148,9 @@ module Reg = struct
let to_string id v =
sprintf "%s -> %s" (id_to_string id) (val_to_string v)
let find id m =
- eprintf "reg_find called with %s\n" (id_to_string id);
+(* eprintf "reg_find called with %s\n" (id_to_string id);*)
let v = find id m in
- eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);
+(* eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);*)
v
end ;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 10:36:41 +0000