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

WIP: Vector Improvements #113

Draft
wants to merge 8 commits into
base: partial_eval
Choose a base branch
from
Draft

WIP: Vector Improvements #113

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
f412e03
Add ITE Simplification Transform
ncough Nov 12, 2024
78b416f
Vector Fixes
ncough Nov 26, 2024
eeba88d
Improve post-dis type inference
ncough Nov 26, 2024
e0e3a03
Rework Shifting
ncough Nov 26, 2024
294c0cb
Vector Rework
ncough Nov 26, 2024
81a15bf
Whitespace in BDDSimp, update tests
ncough Nov 26, 2024
b7e68b2
Extend vectorizer
ncough Nov 26, 2024
ee24298
Guess sqrt impl
ncough Nov 26, 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
5 changes: 5 additions & 0 deletions libASL/asl_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -371,6 +371,11 @@ let calls_of_expr expr =
ignore (visit_expr (cc :> aslVisitor) expr);
cc#result

let calls_of_stmt stmt =
let cc = new callsClass in
ignore (visit_stmt (cc :> aslVisitor) stmt);
cc#result

let calls_of_stmts stmts =
let cc = new callsClass in
ignore (visit_stmts (cc :> aslVisitor) stmts);
Expand Down
7 changes: 6 additions & 1 deletion libASL/dis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,8 @@ let no_inline = [
"BFAdd",0;
"BFMul",0;
"FPRecipEstimate",0;
"FPRSqrtEstimate",0;
"UnsignedRSqrtEstimate",0;
"Mem.read",0;
"Mem.set",0;
"AtomicStart",0;
Expand All @@ -112,6 +114,7 @@ let no_inline_pure () = [
"LSL",0;
"LSR",0;
"ASR",0;
"ROR",0;
"SignExtend",0;
"ZeroExtend",0;
] @ (if !Symbolic.use_vectoriser then [
Expand Down Expand Up @@ -1571,6 +1574,7 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec
let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in
let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in
let stmts' = Transforms.FixRedefinitions.run (globals : IdentSet.t) stmts' in
let stmts' = Loops.LoopNorm.do_transform 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
Expand All @@ -1580,6 +1584,7 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec
let stmts' = Transforms.CaseSimp.do_transform stmts' in
let stmts' = Transforms.RemoveRegisters.run stmts' in
let stmts' = Transforms.AppendZeros.run stmts' in
let stmts' = Transforms.BitITESimp.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
Expand All @@ -1600,7 +1605,7 @@ let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode:
| false -> dis_core env max_upper_bound (lenv,globals) decode op
| true ->
let enc,stmts' = dis_core env Z.one (lenv,globals) decode op in
let (res,stmts') = Transforms.LoopClassify.run stmts' env in
let (res,stmts') = Loops.do_transform stmts' env in
if res then (enc,stmts') else
dis_core env max_upper_bound (lenv,globals) decode op

Expand Down
158 changes: 89 additions & 69 deletions libASL/dis_tc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,29 @@
open Asl_visitor
open Asl_ast
open Asl_utils
open Symbolic

(*
Get the types of expressions in a function body after performing dis.
*)

module LocalVarTypes = struct
let weak_add v t m =
match Bindings.find_opt v m with
| Some t' when t = t' -> m
| None -> Bindings.add v t m
| Some t' ->
failwith @@ "LocalVarTypes: Variable redecl with different type " ^
pprint_ident v ^ ": " ^ pp_type t' ^ " -> " ^ pp_type t

class var_visitor = object
inherit nopAslVisitor
val mutable types = Bindings.empty
method! vstmt s =
(match s with
| Stmt_VarDeclsNoInit(ty, [v], _)
| Stmt_VarDecl(ty, v, _, _)
| Stmt_ConstDecl(ty, v, _, _) -> types <- Bindings.add v ty types
| Stmt_ConstDecl(ty, v, _, _) -> types <- weak_add v ty types
| _ -> ());
DoChildren
method get_types = types
Expand All @@ -28,54 +37,57 @@ module LocalVarTypes = struct
List.fold_right (fun i -> Bindings.add i Value.type_integer) targs types
end

(* Basic ops for bv types *)
let add_int x y = Expr_TApply (FIdent ("add_int", 0), [], [x; y])
let mul_int x y = Expr_TApply (FIdent ("mul_int", 0), [], [x; y])

let prim_type fi targs =
match name_of_FIdent fi, targs with
| ("eq_enum", [ ]) -> Some (Symbolic.type_bool )
| ("ne_enum", [ ]) -> Some (Symbolic.type_bool )
| ("eq_bool", [ ]) -> Some (Symbolic.type_bool )
| ("ne_bool", [ ]) -> Some (Symbolic.type_bool )
| ("or_bool", [ ]) -> Some (Symbolic.type_bool )
| ("and_bool", [ ]) -> Some (Symbolic.type_bool )
| ("implies_bool", [ ]) -> Some (Symbolic.type_bool )
| ("equiv_bool", [ ]) -> Some (Symbolic.type_bool )
| ("not_bool", [ ]) -> Some (Symbolic.type_bool )
| ("eq_int", [ ]) -> Some (Symbolic.type_bool )
| ("ne_int", [ ]) -> Some (Symbolic.type_bool )
| ("le_int", [ ]) -> Some (Symbolic.type_bool )
| ("lt_int", [ ]) -> Some (Symbolic.type_bool )
| ("ge_int", [ ]) -> Some (Symbolic.type_bool )
| ("gt_int", [ ]) -> Some (Symbolic.type_bool )
| ("is_pow2_int", [ ]) -> Some (Symbolic.type_bool )
| ("neg_int", [ ]) -> Some (Value.type_integer )
| ("add_int", [ ]) -> Some (Value.type_integer )
| ("sub_int", [ ]) -> Some (Value.type_integer )
| ("shl_int", [ ]) -> Some (Value.type_integer )
| ("shr_int", [ ]) -> Some (Value.type_integer )
| ("mul_int", [ ]) -> Some (Value.type_integer )
| ("zdiv_int", [ ]) -> Some (Value.type_integer )
| ("zrem_int", [ ]) -> Some (Value.type_integer )
| ("sdiv_int", [ ]) -> Some (Value.type_integer )
| ("fdiv_int", [ ]) -> Some (Value.type_integer )
| ("frem_int", [ ]) -> Some (Value.type_integer )
| ("mod_pow2_int", [ ]) -> Some (Value.type_integer )
| ("align_int", [ ]) -> Some (Value.type_integer )
| ("pow2_int", [ ]) -> Some (Value.type_integer )
| ("pow_int_int", [ ]) -> Some (Value.type_integer )
| ("eq_enum", [ ]) -> Some (type_bool)
| ("ne_enum", [ ]) -> Some (type_bool)
| ("eq_bool", [ ]) -> Some (type_bool)
| ("ne_bool", [ ]) -> Some (type_bool)
| ("or_bool", [ ]) -> Some (type_bool)
| ("and_bool", [ ]) -> Some (type_bool)
| ("implies_bool", [ ]) -> Some (type_bool)
| ("equiv_bool", [ ]) -> Some (type_bool)
| ("not_bool", [ ]) -> Some (type_bool)
| ("eq_int", [ ]) -> Some (type_bool)
| ("ne_int", [ ]) -> Some (type_bool)
| ("le_int", [ ]) -> Some (type_bool)
| ("lt_int", [ ]) -> Some (type_bool)
| ("ge_int", [ ]) -> Some (type_bool)
| ("gt_int", [ ]) -> Some (type_bool)
| ("is_pow2_int", [ ]) -> Some (type_bool)
| ("neg_int", [ ]) -> Some (Value.type_integer)
| ("add_int", [ ]) -> Some (Value.type_integer)
| ("sub_int", [ ]) -> Some (Value.type_integer)
| ("shl_int", [ ]) -> Some (Value.type_integer)
| ("shr_int", [ ]) -> Some (Value.type_integer)
| ("mul_int", [ ]) -> Some (Value.type_integer)
| ("zdiv_int", [ ]) -> Some (Value.type_integer)
| ("zrem_int", [ ]) -> Some (Value.type_integer)
| ("fdiv_int", [ ]) -> Some (Value.type_integer)
| ("frem_int", [ ]) -> Some (Value.type_integer)
| ("mod_pow2_int", [ ]) -> Some (Value.type_integer)
| ("align_int", [ ]) -> Some (Value.type_integer)
| ("pow2_int", [ ]) -> Some (Value.type_integer)
| ("pow_int_int", [ ]) -> Some (Value.type_integer)
| ("round_tozero_real", [ ]) -> Some (Value.type_integer)
| ("round_down_real", [ ]) -> Some (Value.type_integer )
| ("round_up_real", [ ]) -> Some (Value.type_integer )
| ("cvt_bits_sint", [ n]) -> Some (Value.type_integer )
| ("cvt_bits_uint", [ n]) -> Some (Value.type_integer )
| ("eq_real", [ ]) -> Some (Symbolic.type_bool )
| ("ne_real", [ ]) -> Some (Symbolic.type_bool )
| ("le_real", [ ]) -> Some (Symbolic.type_bool )
| ("lt_real", [ ]) -> Some (Symbolic.type_bool )
| ("ge_real", [ ]) -> Some (Symbolic.type_bool )
| ("gt_real", [ ]) -> Some (Symbolic.type_bool )
| ("in_mask", [ n]) -> Some (Symbolic.type_bool )
| ("notin_mask", [ n]) -> Some (Symbolic.type_bool )
| ("eq_bits", [ n]) -> Some (Symbolic.type_bool )
| ("ne_bits", [ n]) -> Some (Symbolic.type_bool )
| ("round_down_real", [ ]) -> Some (Value.type_integer)
| ("round_up_real", [ ]) -> Some (Value.type_integer)
| ("cvt_bits_sint", [ n]) -> Some (Value.type_integer)
| ("cvt_bits_uint", [ n]) -> Some (Value.type_integer)
| ("eq_real", [ ]) -> Some (type_bool)
| ("ne_real", [ ]) -> Some (type_bool)
| ("le_real", [ ]) -> Some (type_bool)
| ("lt_real", [ ]) -> Some (type_bool)
| ("ge_real", [ ]) -> Some (type_bool)
| ("gt_real", [ ]) -> Some (type_bool)
| ("in_mask", [ n]) -> Some (type_bool)
| ("notin_mask", [ n]) -> Some (type_bool)
| ("eq_bits", [ n]) -> Some (type_bool)
| ("ne_bits", [ n]) -> Some (type_bool)
| ("add_bits", [ n]) -> Some (Type_Bits n)
| ("sub_bits", [ n]) -> Some (Type_Bits n)
| ("mul_bits", [ n]) -> Some (Type_Bits n)
Expand All @@ -85,50 +97,58 @@ let prim_type fi targs =
| ("not_bits", [ n]) -> Some (Type_Bits n)
| ("zeros_bits", [ n]) -> Some (Type_Bits n)
| ("ones_bits", [ n]) -> Some (Type_Bits n)
| ("replicate_bits", [n; m ]) -> Some (Type_Bits (Expr_TApply (FIdent ("mul_int", 0), [], [n;m])))
| ("append_bits", [n; m ]) -> Some (Type_Bits (Expr_TApply (FIdent ("add_int", 0), [], [n;m])))
| ("replicate_bits", [n; m ]) -> Some (Type_Bits (mul_int n m))
| ("append_bits", [n; m ]) -> Some (Type_Bits (add_int n m))
| ("cvt_int_bits", [ n]) -> Some (Type_Bits n)
| ("lsl_bits", [ n]) -> Some (Type_Bits n)
| ("lsr_bits", [ n]) -> Some (Type_Bits n)
| ("asr_bits", [ n]) -> Some (Type_Bits n)
| ("sle_bits", [ n]) -> Some (Symbolic.type_bool)
| ("slt_bits", [ n]) -> Some (Symbolic.type_bool)

| ("eq_str", [ ]) -> Some(Symbolic.type_bool)
| ("ne_str", [ ]) -> Some(Symbolic.type_bool)
| ("is_cunpred_exc", [ ]) -> Some(Symbolic.type_bool)
| ("is_exctaken_exc", [ ]) -> Some(Symbolic.type_bool)
| ("is_impdef_exc", [ ]) -> Some(Symbolic.type_bool)
| ("is_see_exc", [ ]) -> Some(Symbolic.type_bool)
| ("is_undefined_exc", [ ]) -> Some(Symbolic.type_bool)
| ("is_unpred_exc", [ ]) -> Some(Symbolic.type_bool)
| ("eq_str", [ ]) -> Some(type_bool)
| ("ne_str", [ ]) -> Some(type_bool)
| ("is_cunpred_exc", [ ]) -> Some(type_bool)
| ("is_exctaken_exc", [ ]) -> Some(type_bool)
| ("is_impdef_exc", [ ]) -> Some(type_bool)
| ("is_see_exc", [ ]) -> Some(type_bool)
| ("is_undefined_exc", [ ]) -> Some(type_bool)
| ("is_unpred_exc", [ ]) -> Some(type_bool)
| ("asl_file_open", [ ]) -> Some(Value.type_integer)
| ("asl_file_getc", [ ]) -> Some(Value.type_integer)
| ("cvt_bool_bv", [ ]) -> Some(Type_Bits(Expr_LitInt("1")))
| ("cvt_bv_bool", [ ]) -> Some(Symbolic.type_bool)
| ("cvt_bv_bool", [ ]) -> Some(type_bool)

| _ -> None

let get_ret_type f targs env =
match Eval.Env.getFun Unknown env f with
| (Some ty,_,targs_s,_,_,_) ->
| (Some ty,_,targs_s,_,_,_) ->
let subst = List.fold_right2 Bindings.add targs_s targs Bindings.empty in
Some (subst_type subst ty)
| _ -> None

let infer_type (e: expr) vars env =
match e with
let eval_type t env =
let eval e = val_expr (Eval.eval_expr Unknown env e) in
match t with
| Some (Type_Bits e) -> Some (Type_Bits (eval e))
| t -> t

let rec infer_type (e: expr) vars env =
let t = match e with
| Expr_Var (Ident "TRUE")
| Expr_Var (Ident "FALSE") -> (Some(Type_Constructor(Ident ("boolean"))))
| Expr_Var v -> Bindings.find_opt v vars
| Expr_Var v ->
(match Bindings.find_opt v vars with
| Some t -> Some t
| None -> Tcheck.GlobalEnv.getGlobalVar (!Tcheck.env0) v)
| 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)))
| Expr_If(ty, c, t, els, e) -> (Some(ty))
| Expr_Unknown(ty) -> (Some(ty))
| Expr_TApply(FIdent("extract_int", 0), _, [_;_;w]) -> (Some(Type_Bits(w)))
| Expr_TApply(f, targs, args) ->
(match prim_type f targs with
| Some t -> Some t
| Some t -> Some t
| None -> get_ret_type f targs env)
| _ -> None
| Expr_Array(a,i) ->
(match infer_type a vars env with
| Some(Type_Array(_,ety)) -> Some ety
| _ -> None)
| _ -> None in
eval_type t env
1 change: 1 addition & 0 deletions libASL/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@
cpp_backend
scala_backend
arm_env pretransforms flags
loops
)
(preprocessor_deps (alias ../asl_files) (alias cpp_backend_files))
(preprocess (pps ppx_blob))
Expand Down
9 changes: 8 additions & 1 deletion libASL/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -502,6 +502,13 @@ let initializeRegistersAndMemory (env: Env.t) (xs: bigint list): unit =
vals
in
Env.setVar Unknown env (Ident "_R") (VArray (arr, d));
let vals = List.mapi (fun i v -> (i, VBits {n=128; v})) xs in
let arr = List.fold_left
(fun a (k,v) -> ImmutableArray.add k v a)
ImmutableArray.empty
vals
in
Env.setVar Unknown env (Ident "_Z") (VArray (arr, d));
let ram = Primops.init_ram (char_of_int 0) in
ram.default <- None;
Env.setVar Unknown env (Ident "__Memory") (VRAM ram)
Expand Down Expand Up @@ -811,7 +818,7 @@ and eval_lexpr (loc: l) (env: Env.t) (x: AST.lexpr) (r: value): unit =
| (s :: ss) ->
let (i, w) = eval_slice loc env s in
let v = extract_bits'' loc r o w in
eval (eval_add_int loc o w) ss (insert_bits loc prev i w v)
eval (eval_add_int loc o w) ss (insert_bits'' loc prev i w v)
)
in
eval_lexpr_modify loc env l (eval (VInt Z.zero) (List.rev ss))
Expand Down
Loading
Loading