Skip to content

Commit

Permalink
Floating Point Fixes
Browse files Browse the repository at this point in the history 
- Remove throws from generated code
- Block inlining on FPRecipEstimate
- Convert enums to bvs as a post-transform
- Alter semantics to permit int/enum comparison, improving coverage testing results
  • Loading branch information
@ncough
ncough committed Feb 22, 2024
1 parent 51d0561 commit 9426a52
Show file tree
Hide file tree
Showing 3 changed files with 124 additions and 51 deletions.
14 changes: 12 additions & 2 deletions libASL/dis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ let no_inline = [
"BFRound",0;
"BFAdd",0;
"BFMul",0;
"FPRecipEstimate",0;
"Mem.read",0;
"Mem.set",0;
"AtomicStart",0;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
149 changes: 102 additions & 47 deletions libASL/transforms.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]) ->
Expand Down Expand Up @@ -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? *)
Expand All @@ -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 =
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down
12 changes: 10 additions & 2 deletions libASL/value.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -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'
Expand Down

0 comments on commit 9426a52

Please sign in to comment.