Skip to content

Commit

Permalink
update pure prim list and move check to after vectoriser
Browse files Browse the repository at this point in the history
  • Loading branch information
@ailrst
ailrst committed Jan 14, 2025
1 parent 643bb1e commit 194a6c8
Show file tree
Hide file tree
Showing 3 changed files with 51 additions and 92 deletions.
25 changes: 9 additions & 16 deletions libASL/dis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1532,15 +1532,7 @@ let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: P
Printf.printf "===========\n";
end;

let suppress = not !check_rasl in
let do_validate () =
try
RASL_check.LoadStatementInvariantExc.check_stmts_exc ~suppress stmts';
RASL_check.AllowedIntrinsicsExc.check_stmts_exc ~suppress stmts';
with
RASL_check.RASLInvariantFailed _ as ex -> raise (DisTrace (lenv'.trace, ex))
in
if not suppress then do_validate ();
RASL_check.LoadStatementInvariantExc.check_stmts_exc ~suppress:(not !check_rasl) stmts';

enc, stmts'

Expand All @@ -1552,13 +1544,14 @@ let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: P
let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list =
let max_upper_bound = Z.of_int64 Int64.max_int in
let config = { eval_env = env ; unroll_bound=max_upper_bound } in
match !Symbolic.use_vectoriser with
| false -> dis_core ~config (lenv,globals) decode op
| true ->
let enc,stmts' = dis_core ~config:{config with unroll_bound= Z.one} (lenv,globals) decode op in
let (res,stmts') = Transforms.LoopClassify.run stmts' env in
if res then (enc,stmts') else
dis_core ~config (lenv,globals) decode op
let stmts = match !Symbolic.use_vectoriser with
| false -> dis_core ~config (lenv,globals) decode op
| true -> let enc,stmts' = dis_core ~config:{config with unroll_bound= Z.one} (lenv,globals) decode op in
let (res,stmts') = Transforms.LoopClassify.run stmts' env in
if res then (enc,stmts') else
dis_core ~config (lenv,globals) decode op
in RASL_check.AllowedIntrinsicsExc.check_stmts_exc ~suppress:(not !check_rasl) (snd stmts);
stmts

let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list =
snd @@ dis_decode_entry_with_inst env (lenv,globals) decode op
Expand Down
90 changes: 14 additions & 76 deletions libASL/rASL_check.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,81 +98,19 @@ module AllowedIntrinsics: InvChecker = struct
(*
Ensure the only intrinsic function calls are appear in the following list.
*)

let impure = List.to_seq (Symbolic.prims_impure ())
let pure = List.to_seq @@ [
FIdent("ite",0);
FIdent("ite_vec",0);
FIdent("Elem.set",0);
FIdent("Elem.read",0);
] @ (Symbolic.prims_pure ())

let allowed_intrinsics =
StringSet.of_list
[
"Mem.read";
"Mem.set";
"Elem.read";
"Elem.set";
"AtomicEnd";
"AtomicStart";
"FPAdd";
"FPDiv";
"FPMul";
"FPMulX";
"FPMulAdd";
"FPMulAddH";
"FPSub";
"FPSqrt";
"FPRSqrtStepFused";
"FPCompare";
"FPCompareGT";
"FPCompareGE";
"FPCompareEQ";
"FPMax";
"FPMin";
"FPMaxNum";
"FPMinNum";
"FPToFixedJS_impl";
"FPRecipEstimate";
"FPRecipStepFused";
"FPRecpX";
"BFAdd";
"BFMul";
"FPCompare";
"FixedToFP";
"FPToFixed";
"FPConvert";
"FPConvertBF";
"FPRoundInt";
"FPRoundIntN";
"not_bool";
"and_bool";
"or_bool";
"cvt_bool_bv";
"SignExtend";
"ZeroExtend";
"add_bits";
"and_bits";
"append_bits";
"asr_bits";
"lsl_bits";
"lsr_bits";
"cvt_bits_uint";
"eor_bits";
"eq_bits";
"ne_bits";
"ite";
"mul_bits";
"not_bits";
"or_bits";
"sdiv_bits";
"sub_bits";
"sle_bits";
"slt_bits";
"replicate_bits";
"select_vec";
"ite_vec";
"eq_vec";
"add_vec";
"sub_vec";
"asr_vec";
"trunc_vec";
"zcast_vec";
"shuffle_vec";
"scast_vec";
]
IdentSet.add_seq pure @@
IdentSet.add_seq impure @@
IdentSet.of_list []

class allowed_intrinsics (vars) = object (self)
inherit Asl_visitor.nopAslVisitor
Expand All @@ -183,7 +121,7 @@ module AllowedIntrinsics: InvChecker = struct
method get_violating () = violating

method!vexpr e = match e with
| Expr_TApply(f, _, _) when (not @@ StringSet.mem (name_of_FIdent f) allowed_intrinsics) -> (
| Expr_TApply(f, _, _) when (not @@ IdentSet.mem f allowed_intrinsics) -> (
let f = (name_of_FIdent f) in
violating <- {at_statement=curstmt; violation=(`DisallowedIntrinsic f)}::violating ;
DoChildren
Expand All @@ -193,7 +131,7 @@ module AllowedIntrinsics: InvChecker = struct
method!vstmt s =
curstmt <- Some s ;
match s with
| Stmt_TCall(f, _, _, _) when (not @@ StringSet.mem (name_of_FIdent f) allowed_intrinsics) ->
| Stmt_TCall(f, _, _, _) when (not @@ IdentSet.mem f allowed_intrinsics) ->
let f = (name_of_FIdent f) in
violating <- {at_statement=curstmt; violation=(`DisallowedIntrinsic f)}::violating ;
DoChildren
Expand Down
28 changes: 28 additions & 0 deletions libASL/symbolic.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -942,6 +942,34 @@ let prims_pure () =
FIdent("slt_bits",0);
FIdent("sle_bits",0);
FIdent("sdiv_bits",0);
FIdent("add_bits",0);
FIdent("and_bits",0);
FIdent("eor_bits",0);
FIdent("eq_bits",0);
FIdent("ne_bits",0);
FIdent("mul_bits",0);
FIdent("not_bits",0);
FIdent("or_bits",0);
FIdent("sub_bits",0);
FIdent("replicate_bits",0);
FIdent("append_bits",0);
FIdent("not_bool",0);
FIdent("and_bool",0);
FIdent("or_bool",0);
FIdent("cvt_bool_bv",0);
FIdent("cvt_bits_uint",0);
FIdent("cvt_bits_sint",0);
FIdent("cvt_uint_bits",0);
FIdent("cvt_int_bits",0);
FIdent("select_vec",0);
FIdent("eq_vec",0);
FIdent("add_vec",0);
FIdent("sub_vec",0);
FIdent("asr_vec",0);
FIdent("trunc_vec",0);
FIdent("zcast_vec",0);
FIdent("shuffle_vec",0);
FIdent("scast_vec",0);
] @ (if !use_vectoriser then [
FIdent("Elem.set",0);
FIdent("Elem.read",0);
Expand Down

0 comments on commit 194a6c8

Please sign in to comment.