diff --git a/bin/asli.ml b/bin/asli.ml index c0e9d5af..567c174f 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -25,7 +25,7 @@ let opt_print_version = ref false let opt_no_default_aarch64 = ref false let opt_export_aarch64_dir = ref "" let opt_verbose = ref false - +let opt_check_rasl = ref false let () = @@ -134,7 +134,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 (try (* Generate and evaluate partially evaluated instruction *) - let disStmts = Dis.dis_decode_entry disEnv lenv decoder op in + let disStmts = Dis.dis_decode_entry disEnv lenv (!opt_check_rasl) decoder op in List.iter (eval_stmt disEvalEnv) disStmts; if Eval.Env.compare evalEnv disEvalEnv then @@ -191,7 +191,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let cpu' = Cpu.mkCPU cpu.env cpu.denv in let op = Z.of_string opcode in Printf.printf "Decoding instruction %s %s\n" iset (Z.format "%x" op); - cpu'.sem iset op + cpu'.sem ~validate_rasl:(!opt_check_rasl) iset op | ":ast" :: iset :: opcode :: rest when List.length rest <= 1 -> let op = Z.of_string opcode in let decoder = Eval.Env.getDecoder cpu.env (Ident iset) in @@ -199,7 +199,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let chan = Option.value chan_opt ~default:stdout in List.iter (fun s -> Printf.fprintf chan "%s\n" (Utils.to_string (PP.pp_raw_stmt s))) - (Dis.dis_decode_entry cpu.env cpu.denv decoder op); + (Dis.dis_decode_entry cpu.env cpu.denv (!opt_check_rasl) decoder op); Option.iter close_out chan_opt | ":gen" :: iset :: id :: rest when List.length rest <= 3 -> let pc_option = Option.value List.(nth_opt rest 1) ~default:"false" in @@ -230,7 +230,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let cpu' = Cpu.mkCPU (Eval.Env.copy cpu.env) cpu.denv in let op = Z.of_string opcode in let decoder = Eval.Env.getDecoder cpu'.env (Ident iset) in - let stmts = Dis.dis_decode_entry cpu'.env cpu.denv decoder op in + let stmts = Dis.dis_decode_entry cpu'.env cpu.denv (!opt_check_rasl) decoder op in let chan = open_out_bin fname in Printf.printf "Dumping instruction semantics for %s %s" iset (Z.format "%x" op); Printf.printf " to file %s\n" fname; @@ -302,6 +302,7 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit = let options = Arg.align ([ ( "-x", Arg.Set_int Dis.debug_level, " Partial evaluation debugging (requires debug level argument >= 0)"); + ( "--check", Arg.Set opt_check_rasl, " Produce an error when rASL does not conform to expected properties"); ( "-v", Arg.Set opt_verbose, " Verbose output"); ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics"); ( "--export-aarch64", Arg.Set_string opt_export_aarch64_dir, " Export bundled AArch64 MRA to the given directory"); diff --git a/bin/server.ml b/bin/server.ml index 759eee24..b8265019 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -24,7 +24,7 @@ let eval_instr (opcode: string) : string * string = let env' = Lazy.force persistent_env in let lenv = Dis.build_env env' in let decoder = Eval.Env.getDecoder env' (Ident "A64") in - let (enc,stmts) = Dis.dis_decode_entry_with_inst env' lenv decoder (Z.of_string opcode) in + let (enc,stmts) = Dis.dis_decode_entry_with_inst env' lenv decoder true (Z.of_string opcode) in let stmts' = List.map pp_raw stmts in enc, String.concat "\n" stmts' diff --git a/libASL/cpu.ml b/libASL/cpu.ml index ec28aa4f..4c226c07 100644 --- a/libASL/cpu.ml +++ b/libASL/cpu.ml @@ -25,7 +25,7 @@ type cpu = { setPC : Primops.bigint -> unit; elfwrite : Int64.t -> char -> unit; opcode : string -> Primops.bigint -> unit; - sem : string -> Primops.bigint -> unit; + sem : validate_rasl:bool -> string -> Primops.bigint -> unit; gen : string -> string -> bool -> gen_backend -> string -> unit; } @@ -55,11 +55,11 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu = let decoder = Eval.Env.getDecoder env (Ident iset) in Eval.eval_decode_case AST.Unknown env decoder opcode - and sem (iset: string) (opcode: Primops.bigint): unit = + and sem ~(validate_rasl:bool) (iset: string) (opcode: Primops.bigint): unit = let decoder = Eval.Env.getDecoder env (Ident iset) in List.iter (fun s -> Printf.printf "%s\n" (pp_stmt s)) - (Dis.dis_decode_entry env denv decoder opcode) + (Dis.dis_decode_entry env denv validate_rasl decoder opcode) and gen (iset: string) (pat: string) (include_pc: bool) (backend: gen_backend) (dir: string): unit = if not (Sys.file_exists dir) then failwith ("Can't find target dir " ^ dir); diff --git a/libASL/cpu.mli b/libASL/cpu.mli index 54801332..983eb1d2 100644 --- a/libASL/cpu.mli +++ b/libASL/cpu.mli @@ -21,7 +21,7 @@ type cpu = { setPC : Primops.bigint -> unit; elfwrite : Int64.t -> char -> unit; opcode : string -> Primops.bigint -> unit; - sem : string -> Primops.bigint -> unit; + sem : validate_rasl:bool -> string -> Primops.bigint -> unit; gen : string -> string -> bool -> gen_backend -> string -> unit; } diff --git a/libASL/dis.ml b/libASL/dis.ml index 930e32d2..a52ee390 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -279,6 +279,7 @@ let rec flatten x acc = type config = { eval_env: Eval.Env.t; unroll_bound: Z.t; + validate_rasl: bool; } module DisEnv = struct @@ -1499,10 +1500,8 @@ let enum_types env i = | _ -> None (* Actually perform dis *) -let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list = +let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list = let DecoderCase_Case (_,_,loc) = decode in - let config = { eval_env = env ; unroll_bound } in - let (enc,lenv',stmts) = (dis_decode_case loc decode op) config lenv in let varentries = List.(concat @@ map (fun vars -> StringMap.(bindings (map fst vars))) lenv.locals) in let bindings = Asl_utils.Bindings.of_seq @@ List.to_seq @@ List.map (fun (x,y) -> (Ident x,y)) varentries in @@ -1511,7 +1510,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' = Transforms.StatefulIntToBits.run (enum_types env) stmts' in + let stmts' = Transforms.StatefulIntToBits.run (enum_types config.eval_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 @@ -1528,6 +1527,16 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec List.iter (fun s -> Printf.printf "%s\n" (pp_stmt s)) stmts'; Printf.printf "===========\n"; end; + + (try + let suppress = not config.validate_rasl in + 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)) + ) + ; + enc, stmts' @@ -1535,18 +1544,19 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec This is a complete hack, but it is nicer to make the loop unrolling decision during partial evaluation, rather than having to unroll after we know vectorization failed. *) -let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list = +let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) validate_rasl (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 ; validate_rasl } in match !Symbolic.use_vectoriser with - | false -> dis_core env max_upper_bound (lenv,globals) decode op + | false -> dis_core ~config (lenv,globals) decode op | true -> - let enc,stmts' = dis_core env Z.one (lenv,globals) decode op in + 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 env max_upper_bound (lenv,globals) decode op + dis_core ~config (lenv,globals) decode op -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 +let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) validate_rasl (decode: decode_case) (op: Primops.bigint): stmt list = + snd @@ dis_decode_entry_with_inst env (lenv,globals) decode validate_rasl op let build_env (env: Eval.Env.t): env = let env = Eval.Env.freeze env in @@ -1585,10 +1595,10 @@ let setPC (env: Eval.Env.t) (lenv,g: env) (address: Z.t): env = let addr = VBits (Primops.mkBits width address) in LocalEnv.setVar loc (Var(0, pc)) (Val addr) lenv,g -let retrieveDisassembly ?(address:string option) (env: Eval.Env.t) (lenv: env) (opcode: string) : stmt list = +let retrieveDisassembly ?(validate_rasl=false) ?(address:string option) (env: Eval.Env.t) (lenv: env) (opcode: string) : stmt list = let decoder = Eval.Env.getDecoder env (Ident "A64") in let DecoderCase_Case (_,_,loc) = decoder in let lenv = match address with | Some v -> setPC env lenv (Z.of_string v) | None -> lenv in - dis_decode_entry env lenv decoder (Z.of_string opcode) + dis_decode_entry env lenv validate_rasl decoder (Z.of_string opcode) diff --git a/libASL/dune b/libASL/dune index 6ebc82e3..80dcf748 100644 --- a/libASL/dune +++ b/libASL/dune @@ -37,6 +37,7 @@ (:standard -w -27 -cclib -lstdc++ -open LibASL_stage0)) (modules cpu dis elf eval lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value + rASL_check symbolic_lifter decoder_program call_graph req_analysis offline_transform dis_tc offline_opt ocaml_backend diff --git a/libASL/rASL_check.ml b/libASL/rASL_check.ml new file mode 100644 index 00000000..ee524dc1 --- /dev/null +++ b/libASL/rASL_check.ml @@ -0,0 +1,198 @@ + + +module AST = Asl_ast +module Env = Eval.Env + +open AST +open Visitor +open Asl_utils +open Asl_visitor + +(**************************************************************** + * Check invariants of the reduced asl language + ****************************************************************) + +type error_info = { + at_statment: stmt option; + violation: [`LoadSingle | `DisallowedIntrinsic of string]; +} + +let show_violation = function + | `LoadSingle -> "Loads are limited to rhs of constdecl" + | `DisallowedIntrinsic s -> "Illegal intrinsic :'" ^ s ^ "'" + +let show_error_info (e: error_info) = + Printf.sprintf "%s at %s" (show_violation e.violation) + ((Option.map (fun s -> pp_stmt s) e.at_statment) |> function | Some x -> x | None -> "") + +exception RASLInvariantFailed of (error_info list) + +let () = Printexc.register_printer (function + | RASLInvariantFailed es -> Some (Printf.sprintf "RASL invariant(s) failed: %s" (String.concat "; " (List.map show_error_info es))) + | _ -> None + ) + +module type InvChecker = sig + val check_stmts : stmt list -> error_info list + val check_expr : expr -> error_info list + val check_stmt : stmt -> error_info list +end + + +module type InvCheckerExc = sig + include InvChecker + val check_stmts_exc : ?suppress:bool -> stmt list -> unit +end + +module MakeInvCheckerExc(E : InvChecker) : InvCheckerExc = struct + include E + + let check_stmts_exc ?(suppress=false) s = if (not suppress) then check_stmts s |> + function + | [] -> () + | es -> raise (RASLInvariantFailed es) +end + +module LoadStatmentInvariant : InvChecker = struct + + class single_load (vars) = object (self) + inherit Asl_visitor.nopAslVisitor + (* Ensures loads only appear in statements of the form lhs := Mem_load(v) *) + + val mutable violating = [] + val mutable curstmt = None + method get_violating () = violating + + method!vexpr e = match e with + | Expr_TApply(f, _, _) when (name_of_FIdent f = "Mem.read") -> ( + violating <- {at_statment=curstmt; violation=`LoadSingle}::violating ; + SkipChildren + ) + | _ -> DoChildren + + method!vstmt s = + curstmt <- Some s ; + match s with + | Stmt_ConstDecl(t, ident, Expr_TApply(f, _, _), loc) when (name_of_FIdent f = "Mem.read") -> SkipChildren + | _ -> DoChildren + + end + + let check_stmts s = + let v = new single_load () in + ignore @@ visit_stmts v s ; + v#get_violating () + + let check_stmt s = check_stmts [s] + + let check_expr e = + let v = new single_load () in + ignore @@ visit_expr v e ; + v#get_violating () + +end + +module AllowedIntrinsics: InvChecker = struct + + (* + Ensure the only intrinsic function calls are appear in the following list. + *) + let allowed_intrinsics = + StringSet.of_list + [ + "Mem.read"; + "Mem.set"; + "Elem.read"; + "Elem.set"; + "AtomicEnd"; + "AtomicStart"; + "FPAdd"; + "FPDiv"; + "FPMul"; + "FPMulAdd"; + "FPSub"; + "FPSqrt"; + "FPCompare"; + "FixedToFP"; + "FPToFixed"; + "FPConvert"; + "FPRoundInt"; + "not_bool"; + "and_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"; + "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"; + ] + + class allowed_intrinsics (vars) = object (self) + inherit Asl_visitor.nopAslVisitor + (* Ensures loads only appear in statements of the form lhs := Mem_load(v) *) + + val mutable violating = [] + val mutable curstmt = None + method get_violating () = violating + + method!vexpr e = match e with + | Expr_TApply(f, _, _) when (not @@ StringSet.mem (name_of_FIdent f) allowed_intrinsics) -> ( + let f = (name_of_FIdent f) in + violating <- {at_statment=curstmt; violation=(`DisallowedIntrinsic f)}::violating ; + DoChildren + ) + | _ -> DoChildren + + method!vstmt s = + curstmt <- Some s ; + match s with + | Stmt_ConstDecl(t, ident, Expr_TApply(f, _, _), loc) when (name_of_FIdent f = "Mem.read") -> SkipChildren + | Stmt_TCall(f, _, _, _) when (not @@ StringSet.mem (name_of_FIdent f) allowed_intrinsics) -> + let f = (name_of_FIdent f) in + violating <- {at_statment=curstmt; violation=(`DisallowedIntrinsic f)}::violating ; + DoChildren + | _ -> DoChildren + + end + + let check_stmts s = + let v = new allowed_intrinsics () in + ignore @@ visit_stmts v s ; + v#get_violating () + + let check_stmt s = check_stmts [s] + + let check_expr e = + let v = new allowed_intrinsics () in + ignore @@ visit_expr v e ; + v#get_violating () + +end + +module LoadStatementInvariantExc = MakeInvCheckerExc(LoadStatmentInvariant) +module AllowedIntrinsicsExc = MakeInvCheckerExc(AllowedIntrinsics) diff --git a/libASL/rASL_check.mli b/libASL/rASL_check.mli new file mode 100644 index 00000000..bf3a02fb --- /dev/null +++ b/libASL/rASL_check.mli @@ -0,0 +1,31 @@ + +module AST = Asl_ast +module Env = Eval.Env + +open AST + +type error_info = { + at_statment: stmt option; + violation: [`LoadSingle | `DisallowedIntrinsic of string]; +} + +exception RASLInvariantFailed of (error_info list) + +module type InvChecker = sig + val check_stmts : stmt list -> error_info list + val check_expr : expr -> error_info list + val check_stmt : stmt -> error_info list +end + + +module type InvCheckerExc = sig + include InvChecker + val check_stmts_exc : ?suppress:bool -> stmt list -> unit +end + +module MakeInvCheckerExc : functor (E: InvChecker) -> InvCheckerExc + +module LoadStatmentInvariant : InvChecker +module AllowedIntrinsics : InvChecker +module LoadStatementInvariantExc : InvCheckerExc +module AllowedIntrinsicsExc : InvCheckerExc diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index 4a37306c..805531b7 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -287,7 +287,7 @@ let dis_wrapper fn fnsig env = let (lenv,globals) = Dis.build_env env in let body = fnsig_get_body fnsig in let args = fnsig_get_typed_args fnsig in - let config = {Dis.eval_env = env ; unroll_bound = Z.of_int64 Int64.max_int} in + let config = {Dis.eval_env = env ; unroll_bound = Z.of_int64 Int64.max_int; validate_rasl=false} in try (* Setup initial environment based on function arguments *) let lenv = diff --git a/libASL/testing.ml b/libASL/testing.ml index 7843a37b..ed83e3fc 100644 --- a/libASL/testing.ml +++ b/libASL/testing.ml @@ -380,7 +380,7 @@ let op_dis (env: Env.t) (iset: string) (op: Primops.bigint): stmt list opresult let lenv = Dis.build_env env in let decoder = Eval.Env.getDecoder env (Ident iset) in try - let stmts = Dis.dis_decode_entry env lenv decoder op in + let stmts = Dis.dis_decode_entry env lenv true decoder op in Result.Ok stmts with | e -> Result.Error (Op_DisFail e) diff --git a/tests/test_asl.ml b/tests/test_asl.ml index d6449f6a..302aa32d 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -82,7 +82,7 @@ let test_compare env () : unit = (try (* Generate and evaluate partially evaluated instruction *) - let disStmts = Dis.dis_decode_entry disEnv lenv decoder op in + let disStmts = Dis.dis_decode_entry disEnv lenv true decoder op in List.iter (Eval.eval_stmt disEvalEnv) disStmts; compare_env evalEnv disEvalEnv opcode