Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Floating Point Cleanup #48

Merged
merged 3 commits into from
Feb 23, 2024
Merged

Floating Point Cleanup #48

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9426a52
Floating Point Fixes
ncough Feb 21, 2024
63076c7
Update coverage results for new behaviour
ncough Feb 22, 2024
e4b178c
Add total case simplification
ncough Feb 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions libASL/dis.ml
View file
Open in desktop
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,12 +1472,14 @@ 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
let stmts' = Transforms.RedundantSlice.do_transform bindings stmts' in
let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in
let stmts' = Transforms.CaseSimp.do_transform stmts' in

if !debug_level >= 2 then begin
let stmts' = Asl_visitor.visit_stmts (new Asl_utils.resugarClass (!TC.binop_table)) stmts' in
Printf.printf "===========\n";
Expand Down
220 changes: 175 additions & 45 deletions libASL/transforms.ml
View file
Open in desktop
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 @@ -649,14 +673,31 @@ module StatefulIntToBits = struct

| e -> e
in
ChangeDoChildrenPost (e', fun e -> e)
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 Expand Up @@ -1502,3 +1557,78 @@ module CommonSubExprElim = struct
let xs = visit_stmts expression_replacer xs in
xs
end

(* A brute force match for total value mappings, implemented as a series of chained ifs *)
module CaseSimp = struct
module StringMap = Map.Make(String);;

(* Match a 'X = BV_CONSTANT' comparison, returning X and BV_CONSTANT *)
let valid_guard e =
match e with
| Expr_TApply (FIdent ("eq_bits", 0), [Expr_LitInt w], [x; Expr_LitBits b]) ->
Some (int_of_string w, x, b)
| _ -> None

(* Match a 'R := BV_CONSTANT' statement, returning R and BV_CONSTANT *)
let valid_body b =
match b with
| Stmt_Assign (LExpr_Var r, Expr_LitBits c, _) -> Some(r, c)
| _ -> None

(* Match a chain of 'if X = BV_CONSTANT then R := BV_CONSTANT else if ... else assert FALSE'
given specific X and R expressions, returning a map from test values to assigned values *)
let rec match_inner stmt x r =
match stmt with
| Stmt_If (e, [c], [], [f], _) ->
(match valid_guard e, valid_body c, match_inner f x r with
| Some (w, x', b), Some (r', c), Some res when x' = x && r = r' -> Some (StringMap.add b c res)
| _ -> None)
| Stmt_Assert (Expr_Var(Ident "FALSE"), _) -> Some StringMap.empty
| _ -> None

(* Match a chain of 'if X = BV_CONSTANT then R := BV_CONSTANT else if ... else assert FALSE',
returning X, R and a map from test values to assigned values *)
let match_outer stmt =
match stmt with
| Stmt_If (e, [t], [], [f], loc) ->
(match valid_guard e, valid_body t with
| Some (w, x, b), Some (r, c) ->
(match match_inner f x r with
| Some res -> Some (x, r, w, loc, StringMap.add b c res)
| _ -> None)
| _ -> None)
| _ -> None

(* Mapping is total if there is an entry for all possible bv values *)
let is_total w res = Z.to_int (Z.shift_left Z.one w) = (StringMap.cardinal res)

(* Guesses for the possible mapping from key to value. This is incredibly dumb. *)
let fn_guess = [
(fun x y -> x = y),
(fun r x _ loc -> Stmt_Assign(LExpr_Var r, x, loc));
(fun x y -> "0" ^ x = y),
(fun r x w loc ->
let nw = expr_of_int (w + 1) in
Stmt_Assign(LExpr_Var r, expr_prim' "ZeroExtend" [expr_of_int w; nw] [x; nw], loc));
]

class visit_if = object
inherit Asl_visitor.nopAslVisitor

(* Assumes x is pure, as it is referenced within a branch condition *)
method! vstmt (s: stmt): stmt visitAction =
match match_outer s with
| Some (x, r, w, loc, res) when is_total w res ->
(match List.find_opt (fun (test,_) -> StringMap.for_all test res) fn_guess with
| Some (_,fn) -> ChangeTo (fn r x w loc)
| _ -> DoChildren)
| _ -> DoChildren

end

let do_transform (xs: stmt list): stmt list =
let stmt_visitor = new visit_if in
let xs = visit_stmts stmt_visitor xs in
xs

end
12 changes: 10 additions & 2 deletions libASL/value.ml
View file
Open in desktop
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
Loading
Loading