summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem14
-rw-r--r--src/lem_interp/interp_lib.lem2
-rw-r--r--src/lem_interp/pretty_interp.ml14
-rw-r--r--src/lem_interp/printing_functions.ml3
-rw-r--r--src/type_check.ml10
-rw-r--r--src/type_internal.ml56
6 files changed, 72 insertions, 27 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a97f5db..7cdc5149 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -168,13 +168,6 @@ let reg_size reg =
end
end
-let vector_length v = match v with
- | V_vector n inc vals -> List.length vals
- | V_vector_sparse n m inc vals def -> m
- | V_lit _ -> 1
- | _ -> 0
-end
-
(*Constant unit value, for use in interpreter *)
let unitv = V_lit (L_aux L_unit Unknown)
@@ -458,6 +451,13 @@ let rec binary_taint thunk vall valr =
| (vl,vr) -> thunk vl vr
end
+let vector_length v = match (detaint v) with
+ | V_vector n inc vals -> List.length vals
+ | V_vector_sparse n m inc vals def -> m
+ | V_lit _ -> 1
+ | _ -> 0
+end
+
val access_vector : value -> nat -> value
let access_vector v n =
retaint v (match (detaint v) with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index bcacaabc..06aabd46 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -683,6 +683,8 @@ let library_functions direction = [
("gt_vec_unsigned", compare_op_vec (>) Unsigned);
("lteq_vec_unsigned", compare_op_vec (<=) Unsigned);
("gteq_vec_unsigned", compare_op_vec (>=) Unsigned);
+ ("signed", to_num Signed);
+ ("unsigned", to_num Unsigned);
("ltu", compare_op_vec_unsigned (<));
("gtu", compare_op_vec_unsigned (>));
("duplicate", duplicate direction);
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 76f216ee..76e696f9 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -364,13 +364,13 @@ let doc_exp, doc_let =
let default_print _ = brackets (separate_map comma (exp env add_red) exps) in
(match exps with
| [] -> default_print ()
- | E_aux(e,_)::es ->
- (match e with
- | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
- utf8string
- ("0b" ^
- (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps ""))
- | _ -> default_print ()))
+ | es ->
+ if (List.for_all (fun e -> match e with (E_aux(E_lit(L_aux((L_one | L_zero),_)),_)) -> true | _ -> false) es)
+ then
+ utf8string
+ ("0b" ^
+ (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst | L_undef -> "u"^rst) exps ""))
+ else default_print ())
| E_vector_indexed (iexps, (Def_val_aux(default,_))) ->
let default_string =
(match default with
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 60e5359b..57326d46 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -54,7 +54,8 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
| Interp.V_lit(L_aux(L_one, _)) -> "1"
| Interp.V_lit(L_aux(L_undef, _)) -> "u"
| Interp.V_unknown -> "?"
- | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) l))
+ | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false)
+ (List.map Interp.detaint l)))
;;
(* pp the bytes of a Bytevector as a hex value *)
diff --git a/src/type_check.ml b/src/type_check.ml
index db1d8e2d..134a2c6c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -697,7 +697,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let check_parms arg_t lft rht =
match check_exp envs imp_param arg_t (E_aux(E_tuple [lft;rht],(l,NoTyp))) with
| ((E_aux(E_tuple [lft';rht'],_)),arg_t,_,cs',_,ef') -> (lft',rht',arg_t,cs',ef')
- | _ -> raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") in
+ | _ ->
+ raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple")
+ in
let check_result ret imp tag cs ef lft rht =
match imp with
(*| IP_length _ ->
@@ -724,14 +726,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
let ret_t,cs_r',ef_r,e' = check_result ret imp tag cs ef lft' rht' in
(e',ret_t,t_env,cs@cs_p@cs_r',nob,union_effects ef (union_effects ef_p ef_r))
- | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
+ | _ ->
+ typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
| Some(Overload(Base((params,t),tag,cs,ef,_),overload_return,variants)) ->
let t_p,cs_p,ef_p,_ = subst params false t cs ef in
let lft',rht',arg_t,arg_cs,arg_ef =
(match t_p.t with
| Tfn(arg,ret,_,ef') -> check_parms arg lft rht
- | _ -> typ_error l ("Expected a function or constructor, found identifier " ^
- i ^ " bound to type " ^ (t_to_string t))) in
+ | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
(*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" i (t_to_string t_p) (t_to_string arg_t) in*)
(match (select_overload_variant d_env true overload_return variants arg_t) with
| [] ->
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 9534f70f..9b3eab6d 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1550,6 +1550,22 @@ let initial_typ_env =
mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
External (Some "lt_vec_signed"),[],pure_e,nob);
]));
+ ("<_u",
+ Overload(
+ Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
+ External (Some "lt"),[],pure_e,nob),
+ false,
+ [Base(((mk_nat_params ["n"; "m"; "o";"p"]),
+ (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
+ External (Some "lt_unsigned"),
+ [LtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_add (mk_nv "n") n_one, mk_nv "o");
+ LtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_add (mk_nv "m") n_one, mk_nv "p")],
+ pure_e,nob);
+ Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+ mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
+ External (Some "lt_vec_unsigned"),[],pure_e,nob);
+ ]));
(">",
Overload(
Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
@@ -1586,6 +1602,22 @@ let initial_typ_env =
mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
External (Some "gt_vec_signed"),[],pure_e,nob);
]));
+ (">_u",
+ Overload(
+ Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
+ External (Some "gt"),[],pure_e,nob),
+ false,
+ [Base(((mk_nat_params ["n";"m";"o";"p"]),
+ (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
+ External (Some "gt_unsigned"),
+ [GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "n", mk_add (mk_nv "o") n_one);
+ GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_add (mk_nv "p") n_one)],
+ pure_e,nob);
+ Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+ mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
+ External (Some "gt_vec_unsigned"),[],pure_e,nob);
+ ]));
("<=",
Overload(
Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
@@ -1650,15 +1682,23 @@ let initial_typ_env =
mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
External (Some "gteq_vec_signed"),[],pure_e,nob);
]));
- (*Unlikely to be the correct type; probably needs to be bit vectors*)
- ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
- External (Some "ltu"),[],pure_e,nob));
- ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
- External (Some "ltu"),[],pure_e,nob));
- (">_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
- External (Some "gtu"),[],pure_e,nob));
("is_one",Base(([],(mk_pure_fun bit_t bit_t)),External (Some "is_one"),[],pure_e,nob));
- (*correct again*)
+ ("signed",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})],
+ (mk_pure_fun (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"))
+ (mk_atom (mk_nv "o")))),
+ External (Some "signed"),
+ [(GtEq(Specc(Parse_ast.Int("signed",None)),Guarantee,
+ mk_nv "o", {nexp = Nneg({nexp = N2n(mk_nv "m",None)})}));
+ (LtEq(Specc(Parse_ast.Int("signed",None)),Guarantee,
+ mk_nv "o", mk_sub {nexp = N2n(mk_nv "m",None)} n_one));],pure_e,nob));
+ ("unsigned",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})],
+ (mk_pure_fun (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"))
+ (mk_atom (mk_nv "o")))),
+ External (Some "unsigned"),
+ [(GtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee,
+ mk_nv "o", n_zero));
+ (LtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee,
+ mk_nv "o", mk_sub {nexp = N2n(mk_nv "m",None)} n_one));],pure_e,nob));
mk_bitwise_op "bitwise_not" "~" 1;
mk_bitwise_op "bitwise_or" "|" 2;
mk_bitwise_op "bitwise_xor" "^" 2;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:02:39 +0000