diff --git a/libASL/dis.ml b/libASL/dis.ml index 65a7be80..96396ceb 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -99,6 +99,7 @@ let no_inline = [ "BFRound",0; "BFAdd",0; "BFMul",0; + "FPRecipEstimate",0; "Mem.read",0; "Mem.set",0; "AtomicStart",0; @@ -1264,7 +1265,7 @@ and dis_stmt' (x: AST.stmt): unit rws = (* cannot throw here because this may be reached by disassembling a case with unknown expressions. should only throw an exception at runtime if does not match. *) - | None -> DisEnv.write [Stmt_Throw (Ident "UNMATCHED CASE", loc)] + | None -> DisEnv.write [Stmt_Assert (expr_false, loc)] | Some s -> dis_stmts s) | Alt_Alt(ps, oc, s) :: alts' -> let pat = (sym_exists (dis_pattern loc v) ps) in @@ -1453,6 +1454,15 @@ and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: type env = (LocalEnv.t * IdentSet.t) + +(* Map enum type idents to the width required to represent them, mapping other idents to None *) +let enum_types env i = + if i = Ident "boolean" then None + else + match Eval.Env.getEnum env i with + | Some l -> Some (Z.log2up (Z.of_int (List.length l))) + | _ -> None + let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: value): stmt list = let DecoderCase_Case (_,_,loc) = decode in let ((),lenv',stmts) = (dis_decode_case loc decode op) env lenv in @@ -1462,7 +1472,7 @@ let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_cas let stmts = flatten stmts [] in let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in - let stmts' = Transforms.StatefulIntToBits.run stmts' in + let stmts' = Transforms.StatefulIntToBits.run (enum_types env) stmts' in let stmts' = Transforms.IntToBits.ints_to_bits stmts' in let stmts' = Transforms.CommonSubExprElim.do_transform stmts' in let stmts' = Transforms.CopyProp.copyProp stmts' in diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 5b9562d8..e5c9e35a 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -447,6 +447,15 @@ module StatefulIntToBits = struct let (_,l) = interval abs in Z.geq l Z.zero + (** Integer variable reads that are successfully converted into + bitvectors are wrapped in the following function call and + subsequently unwrapped in a later pass. + + Variable reads that are not wrapped imply a integer variable + use that this analysis fails to match. To remain compatible, + these variable reads are subsequently converted back to integers. *) + let wrapper_ident = FIdent ("StatefulIntToBit_wrapper", 0) + (** Covert an integer expression tree into a bitvector equivalent *) let rec bv_of_int_expr (vars: state) (e: expr): (sym * abs) = match e with @@ -461,7 +470,7 @@ module StatefulIntToBits = struct (* Assume variables have been declared at this point *) | Expr_Var i -> (match Bindings.find_opt i (snd vars) with - | Some v -> (sym_of_expr e, v) + | Some v -> (sym_prim wrapper_ident [] [Exp e], v) | _ -> failwith @@ "bv_of_int_expr: Unknown identifier: " ^ (pprint_ident i)) | Expr_TApply (FIdent ("cvt_bits_uint", 0), [t], [e]) -> @@ -634,6 +643,21 @@ module StatefulIntToBits = struct let ex x = sym_expr (extend w x) in expr_prim' "slt_bits" [expr_of_abs w] [ex x;ex y] + (* Translation from enum to bit *) + | Expr_TApply (FIdent ("eq_enum", n), [], [x;y]) when n > 0 -> + let x = bv_of_int_expr vars x in + let y = bv_of_int_expr vars y in + let w = merge_abs (snd x) (snd y) in + let ex = extend w in + (sym_expr @@ sym_prim (FIdent ("eq_bits", 0)) [sym_of_abs w] [ex x; ex y]) + + | Expr_TApply (FIdent ("ne_enum", n), [], [x;y]) when n > 0 -> + let x = bv_of_int_expr vars x in + let y = bv_of_int_expr vars y in + let w = merge_abs (snd x) (snd y) in + let ex = extend w in + (sym_expr @@ sym_prim (FIdent ("ne_bits", 0)) [sym_of_abs w] [ex x; ex y]) + (* these functions take bits as first argument and integer as second. just coerce second to bits. *) (* TODO: primitive implementations of these expressions expect the shift amount to be signed, but a negative shift is invalid anyway. Can't it just be unsigned? *) @@ -647,16 +671,33 @@ module StatefulIntToBits = struct let (n,w) = force_signed (bv_of_int_expr vars n) in expr_prim' "asr_bits" [size; expr_of_abs w] [x;sym_expr n] - | e -> e - in - ChangeDoChildrenPost (e', fun e -> e) + | e -> e in + ChangeDoChildrenPost(e', fun e -> e) + end + + (** Cleanup pass to remove wrapper and introduce necessary bit->int conversions *) + class cleanup (vars) = object (self) + inherit Asl_visitor.nopAslVisitor + method! vexpr e = + match e with + | Expr_TApply (f, [], [e]) when f = wrapper_ident -> + ChangeTo e + | Expr_Var v -> + (match Bindings.find_opt v vars with + | Some w -> + (*Printf.printf "transform_int_expr: Found root var: %s\n" (match v with Ident s -> s | _ -> "");*) + let prim = if signed w then "cvt_bits_int" else "cvt_bits_uint" in + ChangeTo (expr_prim' prim [expr_of_abs w] [e]) + | None -> SkipChildren) + | _ -> DoChildren end (** Get a variable's abstract rep with a default initial value *) - let get_default (v: ident) ((_,vars): state): abs = - match Bindings.find_opt v vars with - | Some (a,b,_) -> (a,b,(Z.zero,Z.zero)) - | _ -> abs_of_const Z.zero + let get_default (v: ident) (w: int option) ((_,vars): state): abs = + match w, Bindings.find_opt v vars with + | Some w, _ -> abs_of_uwidth w + | _, Some (a,b,_) -> (a,b,(Z.zero,Z.zero)) + | _, _ -> abs_of_const Z.zero (** Declare a new variable with an initial abstract rep *) let assign (v: ident) (i: abs) ((f,vars): state): state = @@ -686,40 +727,58 @@ module StatefulIntToBits = struct | None, Some l -> Some l | _, _ -> None) vars1 vars2) + (* Identify variable types to track, possibly with a minimum initial width for enums *) + let capture_type enum_types ty: int option option = + if ty = type_integer then Some None + else match ty with + | Type_Constructor i -> + (match enum_types i with + | Some w -> Some (Some w) + | None -> None) + | _ -> None + (** Statement list walk to establish variable widths and visit all expressions *) (* - TODO: Unique variable names or support multiple decls somehow TODO: This won't respect local scopes within If stmts *) - let rec walk changed (vars: abs Bindings.t) (s: stmt list): (state * stmt list) = + let rec walk enum_types changed (vars: abs Bindings.t) (s: stmt list): (state * stmt list) = List.fold_left (fun (st,acc) stmt -> let stmt = Asl_visitor.visit_stmt (new transform_int_expr st) stmt in let (st,stmt) = (match stmt with (* Match integer writes *) - | Stmt_VarDeclsNoInit(t, [v], loc) when t = type_integer -> - let lhs = get_default v st in - let e = Stmt_VarDeclsNoInit (type_bits (string_of_int (width lhs)), [v], loc) in - let st = assign v lhs st in - (st,e) - | Stmt_ConstDecl(t, v, e, loc) when t = type_integer -> - let lhs = get_default v st in - let rhs = bv_of_int_expr st e in - let w = merge_abs lhs (snd rhs) in - let s = sym_expr (extend w rhs) in - let s = Stmt_ConstDecl (type_bits (string_of_int (width w)), v, s, loc) in - let st = assign v w st in - (st,s) - | Stmt_VarDecl(t, v, e, loc) when t = type_integer -> - let lhs = get_default v st in - let rhs = bv_of_int_expr st e in - let w = merge_abs lhs (snd rhs) in - let s = sym_expr (extend w rhs) in - let s = Stmt_VarDecl (type_bits (string_of_int (width w)), v, s, loc) in - let st = assign v w st in - (st,s) + | Stmt_VarDeclsNoInit(t, [v], loc) -> + (match capture_type enum_types t with + | Some w -> + let lhs = get_default v w st in + let e = Stmt_VarDeclsNoInit (type_bits (string_of_int (width lhs)), [v], loc) in + let st = assign v lhs st in + (st,e) + | None -> (st,stmt)) + | Stmt_ConstDecl(t, v, e, loc) -> + (match capture_type enum_types t with + | Some w -> + let lhs = get_default v w st in + let rhs = bv_of_int_expr st e in + let w = merge_abs lhs (snd rhs) in + let s = sym_expr (extend w rhs) in + let s = Stmt_ConstDecl (type_bits (string_of_int (width w)), v, s, loc) in + let st = assign v w st in + (st,s) + | None -> (st,stmt)) + | Stmt_VarDecl(t, v, e, loc) -> + (match capture_type enum_types t with + | Some w -> + let lhs = get_default v w st in + let rhs = bv_of_int_expr st e in + let w = merge_abs lhs (snd rhs) in + let s = sym_expr (extend w rhs) in + let s = Stmt_VarDecl (type_bits (string_of_int (width w)), v, s, loc) in + let st = assign v w st in + (st,s) + | None -> (st,stmt)) | Stmt_Assign(LExpr_Var(v), e, loc) when tracked v st -> - let lhs = get_default v st in + let lhs = get_default v None st in let rhs = bv_of_int_expr st e in let w = merge_abs lhs (snd rhs) in let s = sym_expr (extend w rhs) in @@ -730,32 +789,28 @@ module StatefulIntToBits = struct (* Expect only normalised Ifs *) | Stmt_If (e, tstmts, [], fstmts, loc) -> let (changed,vars) = st in - let (t,tstmts) = walk changed vars tstmts in - let (f,fstmts) = walk changed vars fstmts in + let (t,tstmts) = walk enum_types changed vars tstmts in + let (f,fstmts) = walk enum_types changed vars fstmts in (merge t f,Stmt_If(e, tstmts, [], fstmts, loc)) | Stmt_If _ -> failwith "walk: invalid if" (* Ignore all other stmts *) - | Stmt_Assert _ - | Stmt_Throw _ - | Stmt_TCall _ | Stmt_VarDeclsNoInit _ - | Stmt_ConstDecl _ - | Stmt_VarDecl _ - | Stmt_Assign _ -> - (st,stmt) + | Stmt_Assign _ + | Stmt_Assert _ + | Stmt_TCall _ -> (st,stmt) | _ -> failwith "walk: invalid IR") in (st,acc@[stmt]) ) ((changed,vars),[]) s - let rec fixedPoint (vars: abs Bindings.t) (s: stmt list): stmt list = - let ((changed,vars),res) = walk false vars s in - if changed then fixedPoint vars s - else res + let rec fixedPoint (enum_types: ident -> int option) (vars: abs Bindings.t) (s: stmt list): stmt list = + let ((changed,vars),res) = walk enum_types false vars s in + if changed then fixedPoint enum_types vars s + else Asl_visitor.visit_stmts (new cleanup vars) res - let run (s: stmt list): stmt list = - fixedPoint Bindings.empty s + let run (enum_types: ident -> int option) (s: stmt list): stmt list = + fixedPoint enum_types Bindings.empty s end diff --git a/libASL/value.ml b/libASL/value.ml index 02ae1e85..e9e1a395 100644 --- a/libASL/value.ml +++ b/libASL/value.ml @@ -253,10 +253,16 @@ let from_stringLit (x: string): value = let eval_prim (f: string) (tvs: value list) (vs: value list): value option = ( match (f, tvs, vs) with - | ("eq_enum", [ ], [VEnum x; VEnum y ]) -> Some (VBool (snd x = snd y)) - | ("eq_enum", [ ], [VBool x; VBool y ]) -> Some (VBool (x = y)) + | ("eq_enum", [ ], [VEnum x; VEnum y ]) -> Some (VBool (snd x = snd y)) + | ("eq_enum", [ ], [VBool x; VBool y ]) -> Some (VBool (x = y)) + | ("eq_enum", [ ], [VEnum x; VInt y ]) -> Some (VBool (snd x = Z.to_int y)) + | ("eq_enum", [ ], [VInt x; VEnum y ]) -> Some (VBool (Z.to_int x = snd y)) + | ("ne_enum", [ ], [VEnum x; VEnum y ]) -> Some (VBool (snd x <> snd y)) | ("ne_enum", [ ], [VBool x; VBool y ]) -> Some (VBool (x <> y)) + | ("ne_enum", [ ], [VEnum x; VInt y ]) -> Some (VBool (snd x <> Z.to_int y)) + | ("ne_enum", [ ], [VInt x; VEnum y ]) -> Some (VBool (Z.to_int x <> snd y)) + | ("eq_bool", [ ], [VBool x; VBool y ]) -> Some (VBool (prim_eq_bool x y)) | ("ne_bool", [ ], [VBool x; VBool y ]) -> Some (VBool (prim_ne_bool x y)) | ("equiv_bool", [ ], [VBool x; VBool y ]) -> Some (VBool (prim_equiv_bool x y)) @@ -416,6 +422,8 @@ let rec eval_eq (loc: AST.l) (x: value) (y: value): bool = (match (x, y) with | (VBool x', VBool y') -> prim_eq_bool x' y' | (VEnum x', VEnum y') -> snd x' = snd y' + | (VEnum x', VInt y') -> snd x' = Z.to_int y' + | (VInt x', VEnum y') -> Z.to_int x' = snd y' | (VInt x', VInt y') -> prim_eq_int x' y' | (VReal x', VReal y') -> prim_eq_real x' y' | (VBits x', VBits y') -> prim_eq_bits x' y'