From eeb0ae82f316dad98b2ee1ad54cdfd4c64eb2808 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 24 Jul 2024 12:13:57 +1000 Subject: [PATCH] Revert "dis: do not emit slices with dynamic indices" This reverts commit 4f7eca7aeafa79b8f01fb90341aa26f527cdff45. --- libASL/dis.ml | 27 +++++++++------------------ libASL/dis_tc.ml | 8 ++------ libASL/symbolic.ml | 11 +++-------- 3 files changed, 14 insertions(+), 32 deletions(-) diff --git a/libASL/dis.ml b/libASL/dis.ml index 9e7d9934..1d7cb52b 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -307,6 +307,7 @@ module LocalEnv = struct | Some (t,_) -> Some (t,v) | None -> internal_error loc @@ "failed to set resolved variable: " ^ pp_var x)) n env.locals in { env with locals } + end type tree = @@ -717,14 +718,7 @@ and type_of_load (loc: l) (x: expr): ty rws = (match Tcheck.derefType env t with | Type_Array(ixty, elty) -> dis_type loc elty | _ -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr a))) - | _ -> - let@ config = DisEnv.read in - let@ lenv = DisEnv.get in - let vars x = Some (fst @@ snd @@ LocalEnv.resolveGetVar loc (Ident x) lenv) in - - match Dis_tc.infer_type' x vars config.eval_env with - | Some t -> dis_type loc t - | None -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr x))) + | _ -> raise (EvalError (loc, "Can't type expression: " ^ pp_expr x))) and type_access_chain (loc: l) (var: var) (ref: access_chain list): ty rws = let Var (_,id) = var in @@ -876,18 +870,15 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws = let+ vs = DisEnv.traverse (fun f -> dis_load_with_type loc (Expr_Field(e,f))) fs in let vs' = List.map (fun (t,x) -> (width_of_type loc t, x)) vs in sym_concat loc vs' + | Expr_Slices(e, [s]) -> + let@ e' = dis_expr loc e in + let+ (i,w) = dis_slice loc s in + sym_extract_bits loc e' i w | Expr_Slices(e, ss) -> - let@ config = DisEnv.read in - let@ ty = type_of_load loc e in let@ e' = dis_expr loc e in let+ ss' = DisEnv.traverse (dis_slice loc) ss in - (match ty with - | Type_Constructor (Ident "integer") -> - Exp (Expr_Slices(sym_expr e', List.map (fun (x,y) -> Slice_LoWd(sym_expr x,sym_expr y)) ss')) - | _ -> - let vwd = width_of_type loc ty in - let vs = List.map (fun (i,w) -> (int_of_sym w, sym_extract_bits loc e' vwd i w)) ss' in - sym_concat loc vs) + let vs = List.map (fun (i,w) -> (int_of_sym w, sym_extract_bits loc e' i w)) ss' in + sym_concat loc vs | Expr_In(e, p) -> let@ e' = dis_expr loc e in let@ p' = dis_pattern loc e' p in @@ -1210,7 +1201,7 @@ and dis_lexpr' (loc: l) (x: lexpr) (r: sym): unit rws = | [] -> DisEnv.pure prev | (s :: ss) -> let@ (i, w) = dis_slice loc s in - let v = sym_extract_bits loc r prev_width o w in + let v = sym_extract_bits loc r o w in eval (sym_add_int loc o w) ss (sym_insert_bits loc prev_width prev i w v) ) in diff --git a/libASL/dis_tc.ml b/libASL/dis_tc.ml index 0fa763f2..39609f15 100644 --- a/libASL/dis_tc.ml +++ b/libASL/dis_tc.ml @@ -116,11 +116,11 @@ let get_ret_type f targs env = Some (subst_type subst ty) | _ -> None -let rec infer_type' (e: expr) vars env = +let infer_type (e: expr) vars env = match e with | Expr_Var (Ident "TRUE") | Expr_Var (Ident "FALSE") -> (Some(Type_Constructor(Ident ("boolean")))) - | Expr_Var (Ident v) -> vars v + | Expr_Var v -> Bindings.find_opt v vars | Expr_LitInt _ -> (Some(Value.type_integer)) | Expr_LitBits bv -> (Some(Type_Bits(Expr_LitInt (string_of_int (String.length bv))))) | Expr_Slices(x, [Slice_LoWd(l,w)]) -> (Some(Type_Bits(w))) @@ -131,8 +131,4 @@ let rec infer_type' (e: expr) vars env = (match prim_type f targs with | Some t -> Some t | None -> get_ret_type f targs env) - | Expr_Parens e -> infer_type' e vars env | _ -> None - -let infer_type e vars env = - infer_type' e (fun v -> Bindings.find_opt (Ident v) vars) env diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml index 9ffb89a4..7f09e43f 100644 --- a/libASL/symbolic.ml +++ b/libASL/symbolic.ml @@ -550,7 +550,7 @@ and sym_slice (loc: l) (x: sym) (lo: int) (wd: int): sym = | _ -> Exp slice_expr) (** Wrapper around sym_slice to handle cases of symbolic slice bounds *) -let rec sym_extract_bits loc v vwd i w = +let sym_extract_bits loc v i w = match (v, i, w) with (* Constant slice *) | _, Val i', Val w' -> @@ -560,13 +560,8 @@ let rec sym_extract_bits loc v vwd i w = (* Nested slice *) | Exp (Expr_Slices (e, [Slice_LoWd (lo,wd)])), lo', wd' -> let lo = sym_add_int loc (Exp lo) lo' in - sym_extract_bits loc (sym_of_expr e) vwd lo wd' - (* Lower dynamically-indexed extractions to a shift. Requires static width. *) - | v, Exp lo, Val w -> - let shifted = Exp (Expr_TApply (FIdent ("LSR", 0), [Expr_LitInt (string_of_int vwd)], [sym_expr v; lo])) in - sym_slice loc shifted 0 (to_int loc w) - | _ -> failwith "asjdio" - (* | _ -> Exp (Expr_Slices (sym_expr v, [Slice_LoWd (sym_expr i, sym_expr w)])) *) + Exp (Expr_Slices (e, [Slice_LoWd (sym_expr lo, sym_expr wd')])) + | _ -> Exp (Expr_Slices (sym_expr v, [Slice_LoWd (sym_expr i, sym_expr w)])) let sym_zero_extend num_zeros old_width e = match sym_append_bits Unknown num_zeros old_width (Val (val_zeros num_zeros)) e with