From 535a65099f69f03739071fc8ccb9f127302f03a1 Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Mon, 1 Jul 2024 15:01:23 +1000 Subject: [PATCH] support non 32-bit length opcodes (#89) * support non 32-bit length opcodes this retrofits the eval and dis modules to use a bigint for the opcode during the decode phase, supporting pcodes of arbitrary length and (potentially) variable-length opcodes. once a particular encoding is identified through the decode tree, we convert the bigint to a fixed-width bitvector. this is then passed through to the rest of the evaluation / analysis. * add best-effort error when given opcode is too long this is not robust, as it only triggers if non-zero bits are set above the expected length. after parsing into a bigint, leading zeros become indiscernible. --- bin/asli.ml | 7 +++--- bin/offline_coverage.ml | 2 +- libASL/cpu.ml | 6 ++---- libASL/dis.ml | 29 +++++++++++-------------- libASL/eval.ml | 48 ++++++++++++++++++++++++++--------------- libASL/testing.ml | 26 ++++++++++------------ libASL/value.ml | 7 ++++++ tests/test_asl.ml | 2 +- 8 files changed, 69 insertions(+), 58 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 50d2b6be..20fd6838 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -127,7 +127,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let lenv = Dis.build_env disEnv in let opcode = input_line inchan in - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_int (int_of_string opcode))) in + let op = Z.of_string opcode in (* Printf.printf "PRE Eval env: %s\n\n" (Testing.pp_eval_env evalEnv); Printf.printf "PRE Dis eval env: %s\n\n" (Testing.pp_eval_env disEvalEnv); *) @@ -197,7 +197,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 Printf.printf "Decoding instruction %s %s\n" iset (Z.format "%x" op); cpu'.sem iset op | ":ast" :: iset :: opcode :: rest when List.length rest <= 1 -> - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_string opcode)) in + let op = Z.of_string opcode in let decoder = Eval.Env.getDecoder cpu.env (Ident iset) in let chan_opt = Option.map open_out (List.nth_opt rest 0) in let chan = Option.value chan_opt ~default:stdout in @@ -226,9 +226,8 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 in let cpu' = Cpu.mkCPU (Eval.Env.copy cpu.env) cpu.denv in let op = Z.of_string opcode in - let bits = VBits (Primops.prim_cvt_int_bits (Z.of_int 32) op) in let decoder = Eval.Env.getDecoder cpu'.env (Ident iset) in - let stmts = Dis.dis_decode_entry cpu'.env cpu.denv decoder bits in + let stmts = Dis.dis_decode_entry cpu'.env cpu.denv 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; diff --git a/bin/offline_coverage.ml b/bin/offline_coverage.ml index 6263b6f0..595b8e7a 100644 --- a/bin/offline_coverage.ml +++ b/bin/offline_coverage.ml @@ -18,7 +18,7 @@ let op_dis (op: int): stmt list opresult = | e -> Result.Error (Op_DisFail e) let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = - let op' = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_int op)) in + let op' = Z.of_int op in let initenv = Env.copy env in Random.self_init (); diff --git a/libASL/cpu.ml b/libASL/cpu.ml index 19430dc6..f536fa92 100644 --- a/libASL/cpu.ml +++ b/libASL/cpu.ml @@ -51,16 +51,14 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu = Eval.eval_proccall loc env (AST.FIdent ("__ELFWriteMemory", 0)) [] [a; b] and opcode (iset: string) (opcode: Primops.bigint): unit = - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) opcode) in let decoder = Eval.Env.getDecoder env (Ident iset) in - Eval.eval_decode_case AST.Unknown env decoder op + Eval.eval_decode_case AST.Unknown env decoder opcode and sem (iset: string) (opcode: Primops.bigint): unit = - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) opcode) in 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 op) + (Dis.dis_decode_entry env denv decoder opcode) and gen (iset: string) (pat: string) (backend: gen_backend) (dir: string): unit = if not (Sys.file_exists dir) then failwith ("Can't find target dir " ^ dir); diff --git a/libASL/dis.ml b/libASL/dis.ml index 0d2b3c22..f7b9ed1b 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -1343,15 +1343,12 @@ and dis_stmt' (x: AST.stmt): unit rws = DisEnv.write [Stmt_Assert(expr_false, loc)] ) -let dis_encoding (x: encoding) (op: value): bool rws = +let dis_encoding (x: encoding) (op: Primops.bigint): bool rws = let Encoding_Block (nm, iset, fields, opcode, guard, unpreds, b, loc) = x in (* todo: consider checking iset *) (* Printf.printf "Checking opcode match %s == %s\n" (Utils.to_string (PP.pp_opcode_value opcode)) (pp_value op); *) - let ok = (match opcode with - | Opcode_Bits b -> eval_eq loc op (from_bitsLit b) - | Opcode_Mask m -> eval_inmask loc op (from_maskLit m) - ) in - if ok then begin + match Eval.eval_opcode_guard loc opcode op with + | Some op -> if !Eval.trace_instruction then Printf.printf "TRACE: instruction %s\n" (pprint_ident nm); let@ () = DisEnv.traverse_ (function (IField_Field (f, lo, wd)) -> @@ -1372,13 +1369,12 @@ let dis_encoding (x: encoding) (op: value): bool rws = end else begin DisEnv.pure false end - end else begin - DisEnv.pure false - end + | None -> DisEnv.pure false -let dis_decode_slice (loc: l) (x: decode_slice) (op: value): value rws = +let dis_decode_slice (loc: l) (x: decode_slice) (op: Primops.bigint): value rws = (match x with | DecoderSlice_Slice (lo, wd) -> + let op = Value.from_bitsInt (lo+wd) op in DisEnv.pure @@ extract_bits' loc op lo wd | DecoderSlice_FieldName f -> (* assumes expression always evaluates to concrete value. *) @@ -1390,11 +1386,11 @@ let dis_decode_slice (loc: l) (x: decode_slice) (op: value): value rws = ) (* Duplicate of eval_decode_case modified to print rather than eval *) -let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: value): unit rws = +let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rws = let body = dis_decode_case' loc x op in if no_debug() then body else DisEnv.scope loc "dis_decode_case" (pp_decode_case x) Utils.pp_unit body -and dis_decode_case' (loc: AST.l) (x: decode_case) (op: value): unit rws = +and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rws = (match x with | DecoderCase_Case (ss, alts, loc) -> let@ vs = DisEnv.traverse (fun s -> dis_decode_slice loc s op) ss in @@ -1413,11 +1409,11 @@ and dis_decode_case' (loc: AST.l) (x: decode_case) (op: value): unit rws = ) (* Duplicate of eval_decode_alt modified to print rather than eval *) -and dis_decode_alt (loc: l) (x: decode_alt) (vs: value list) (op: value): bool rws = +and dis_decode_alt (loc: l) (x: decode_alt) (vs: value list) (op: Primops.bigint): bool rws = let body = dis_decode_alt' loc x vs op in if no_debug() then body else DisEnv.scope loc "dis_decode_alt" (pp_decode_alt x) string_of_bool body -and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: value): bool rws = +and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): bool rws = if List.for_all2 (Eval.eval_decode_pattern loc) ps vs then (match b with | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable)) @@ -1461,6 +1457,7 @@ and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: | DecoderBody_Decoder (fs, c, loc) -> let@ () = DisEnv.modify (LocalEnv.addLevel) in let@ () = DisEnv.traverse_ (function (IField_Field (f, lo, wd)) -> + let op = Value.from_bitsInt (lo+wd) op in let v = extract_bits' loc op lo wd in declare_assign_var loc (val_type v) f (Val v) ) fs @@ -1483,7 +1480,7 @@ let enum_types env i = | 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 dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list = let DecoderCase_Case (_,_,loc) = decode in let ((),lenv',stmts) = (dis_decode_case loc decode op) env lenv in let varentries = List.(concat @@ map (fun vars -> StringMap.(bindings (map fst vars))) lenv.locals) in @@ -1553,4 +1550,4 @@ let retrieveDisassembly ?(address:string option) (env: Eval.Env.t) (lenv: env) ( let lenv = match address with | Some v -> setPC env lenv (Z.of_string v) | None -> lenv in - dis_decode_entry env lenv decoder (Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_string opcode))) + dis_decode_entry env lenv decoder (Z.of_string opcode) diff --git a/libASL/eval.ml b/libASL/eval.ml index 39859f6f..d06c4b0b 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -520,13 +520,30 @@ let removeGlobalConsts (env: Env.t) (ids: IdentSet.t): IdentSet.t = (****************************************************************) (** Evaluate bitslice of instruction opcode *) -let eval_decode_slice (loc: l) (env: Env.t) (x: decode_slice) (op: value): value = +let eval_decode_slice (loc: l) (env: Env.t) (x: decode_slice) (op: Primops.bigint): value = (match x with - | DecoderSlice_Slice (lo, wd) -> extract_bits' loc op lo wd + | DecoderSlice_Slice (lo, wd) -> + let op = Value.from_bitsInt (lo+wd) op in + extract_bits' loc op lo wd | DecoderSlice_FieldName f -> Env.getVar loc env f | DecoderSlice_Concat fs -> eval_concat loc (List.map (Env.getVar loc env) fs) ) +(** Evaluate an encoding's opcode guard pattern *) +let eval_opcode_guard (loc: AST.l) (x: opcode_value) (op: Primops.bigint): value option = + let opcode_val, eval_opcode = (match x with + | Opcode_Bits b -> (from_bitsLit b, eval_eq) + | Opcode_Mask m -> (from_maskLit m, eval_inmask) + ) in + let opcode_len = length_bits loc opcode_val in + (* rudimentary length compatibility check. this will only throw if there are *set* bits + exceeding the expected length. *) + if opcode_len < Z.numbits op then + raise (EvalError (loc, Printf.sprintf "opcode too long, expected %d bits but got %d: 0x%s" + opcode_len (Z.numbits op) (Z.format "%x" op))); + let value = from_bitsInt opcode_len op in + if eval_opcode loc value opcode_val then Some value else None + (** Evaluate instruction decode pattern match *) let rec eval_decode_pattern (loc: AST.l) (x: decode_pattern) (op: value): bool = (match x with @@ -910,7 +927,8 @@ and eval_stmt (env: Env.t) (x: AST.stmt): unit = | Stmt_DecodeExecute(i, e, loc) -> let dec = Env.getDecoder env i in let op = eval_expr loc env e in - eval_decode_case loc env dec op + let value = (to_bits loc op).v in + eval_decode_case loc env dec value | Stmt_If(c, t, els, e, loc) -> let rec eval css d = (match css with @@ -1055,7 +1073,7 @@ and eval_proccall (loc: l) (env: Env.t) (f: ident) (tvs: value list) (vs: value ) (** Evaluate instruction decode case *) -and eval_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value): unit = +and eval_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: Primops.bigint): unit = (match x with | DecoderCase_Case (ss, alts, loc) -> let vs = List.map (fun s -> eval_decode_slice loc env s op) ss in @@ -1074,7 +1092,7 @@ and eval_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value): uni ) (** Evaluate instruction decode case alternative *) -and eval_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: value): bool = +and eval_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): bool = if List.for_all2 (eval_decode_pattern loc) ps vs then (match b with | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable)) @@ -1096,6 +1114,7 @@ and eval_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: valu | DecoderBody_Decoder (fs, c, loc) -> (* let env = Env.empty in *) List.iter (function (IField_Field (f, lo, wd)) -> + let op = Value.from_bitsInt (lo+wd) op in Env.addLocalVar loc env f (extract_bits' loc op lo wd) ) fs; eval_decode_case loc env c op; @@ -1105,7 +1124,7 @@ and eval_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: valu false (** Evaluates instruction but draw statements from list, not specification *) -and eval_stmt_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value) (xs: stmt list): unit = +and eval_stmt_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: Primops.bigint) (xs: stmt list): unit = (match x with | DecoderCase_Case (ss, alts, loc) -> let vs = List.map (fun s -> eval_decode_slice loc env s op) ss in @@ -1123,7 +1142,7 @@ and eval_stmt_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value) (xs: s eval alts ) -and eval_stmt_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: value) (xs: stmt list): bool = +and eval_stmt_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint) (xs: stmt list): bool = if List.for_all2 (eval_decode_pattern loc) ps vs then (match b with | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable)) @@ -1145,6 +1164,7 @@ and eval_stmt_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value | DecoderBody_Decoder (fs, c, loc) -> (* let env = Env.empty in *) List.iter (function (IField_Field (f, lo, wd)) -> + let op = Value.from_bitsInt (lo+wd) op in Env.addLocalVar loc env f (extract_bits' loc op lo wd) ) fs; eval_decode_case loc env c op; @@ -1154,15 +1174,12 @@ and eval_stmt_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value false (** Evaluate instruction encoding *) -and eval_encoding (env: Env.t) (x: encoding) (op: value): bool = +and eval_encoding (env: Env.t) (x: encoding) (op: Primops.bigint): bool = let Encoding_Block (nm, iset, fields, opcode, guard, unpreds, b, loc) = x in (* todo: consider checking iset *) (* Printf.printf "Checking opcode match %s == %s\n" (Utils.to_string (PP.pp_opcode_value opcode)) (pp_value op); *) - let ok = (match opcode with - | Opcode_Bits b -> eval_eq loc op (from_bitsLit b) - | Opcode_Mask m -> eval_inmask loc op (from_maskLit m) - ) in - if ok then begin + match eval_opcode_guard loc opcode op with + | Some op -> if !trace_instruction then Printf.printf "TRACE: instruction %s\n" (pprint_ident nm); List.iter (function (IField_Field (f, lo, wd)) -> let v = extract_bits' loc op lo wd in @@ -1179,10 +1196,7 @@ and eval_encoding (env: Env.t) (x: encoding) (op: value): bool = end else begin false end - end else begin - false - end - + | None -> false (****************************************************************) diff --git a/libASL/testing.ml b/libASL/testing.ml index be51e87e..7843a37b 100644 --- a/libASL/testing.ml +++ b/libASL/testing.ml @@ -13,16 +13,13 @@ open Asl_utils These "try" decoding each opcode. *) (** Try to evaluate an "encoding" block to the given opcode. *) -let rec try_encoding (env: Env.t) (x: encoding) (op: value): bool = +let rec try_encoding (env: Env.t) (x: encoding) (op: Primops.bigint): bool = let Encoding_Block (nm, iset, fields, opcode, guard, unpreds, b, loc) = x in (* todo: consider checking iset *) (* Printf.printf "Checking opcode match %s == %s\n" (Utils.to_string (PP.pp_opcode_value opcode)) (pp_value op); *) - let ok = (match opcode with - | Opcode_Bits b -> eval_eq loc op (from_bitsLit b) - | Opcode_Mask m -> eval_inmask loc op (from_maskLit m) - ) in let trace_instruction = ref false in - if ok then begin + match Eval.eval_opcode_guard loc opcode op with + | Some op -> if !trace_instruction then Printf.printf "TRACE: instruction %s\n" (pprint_ident nm); List.iter (function (IField_Field (f, lo, wd)) -> let v = extract_bits' loc op lo wd in @@ -42,12 +39,10 @@ let rec try_encoding (env: Env.t) (x: encoding) (op: value): bool = end else begin false end - end else begin - false - end + | None -> false (** Tests whether the given opcode can be decoded by the given decode case. *) -and try_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value): ident option = +and try_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: Primops.bigint): ident option = (match x with | DecoderCase_Case (ss, alts, loc) -> let vs = List.map (fun s -> Eval.eval_decode_slice loc env s op) ss in @@ -65,7 +60,7 @@ and try_decode_case (loc: AST.l) (env: Env.t) (x: decode_case) (op: value): iden ) (** Tests whether the given opcode is decodable by the given decode case alternative. *) -and try_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: value): ident option = +and try_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): ident option = if List.for_all2 (Eval.eval_decode_pattern loc) ps vs then (match b with | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable)) @@ -81,6 +76,7 @@ and try_decode_alt (loc: AST.l) (env: Env.t) (DecoderAlt_Alt (ps, b)) (vs: value | DecoderBody_Decoder (fs, c, loc) -> (* let env = Env.empty in *) List.iter (function (IField_Field (f, lo, wd)) -> + let op = Value.from_bitsInt (lo+wd) op in Env.addLocalVar loc env f (extract_bits' loc op lo wd) ) fs; try_decode_case loc env c op @@ -152,7 +148,7 @@ let enumerate_opcodes (env: Env.t) (case: decode_case) start stop fname: unit = while !i <> stop do let opresult = - (try try_decode_case Unknown env case (VBits {n=32; v=Z.of_int !i}) + (try try_decode_case Unknown env case (Z.of_int !i) with Throw _ -> None) in (match opresult with @@ -370,7 +366,7 @@ type 'a opresult = ('a, operror) Result.t let pp_opresult f = Result.fold ~ok:f ~error:pp_operror -let op_eval (env: Env.t) (iset: string) (op: value): Env.t opresult = +let op_eval (env: Env.t) (iset: string) (op: Primops.bigint): Env.t opresult = let evalenv = Env.copy env in let decoder = Eval.Env.getDecoder evalenv (Ident iset) in try @@ -379,7 +375,7 @@ let op_eval (env: Env.t) (iset: string) (op: value): Env.t opresult = with | e -> Result.Error (Op_EvalFail e) -let op_dis (env: Env.t) (iset: string) (op: value): stmt list opresult = +let op_dis (env: Env.t) (iset: string) (op: Primops.bigint): stmt list opresult = let env = Env.copy env in let lenv = Dis.build_env env in let decoder = Eval.Env.getDecoder env (Ident iset) in @@ -404,7 +400,7 @@ let op_compare ((evalenv, disenv): Env.t * Env.t): Env.t opresult = Result.Error (Op_DisEvalNotEqual) let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_int op)) in + let op = Z.of_int op in let initenv = Env.copy env in Random.self_init (); diff --git a/libASL/value.ml b/libASL/value.ml index 48135b11..1e7e6232 100644 --- a/libASL/value.ml +++ b/libASL/value.ml @@ -209,6 +209,9 @@ let from_realLit (x: AST.realLit): value = let denominator = Z.pow (Z.of_int 10) fracsz in VReal (Q.make numerator denominator) +let from_bitsInt (wd: int) (x: Primops.bigint) = + VBits (Primops.mkBits wd x) + let from_bitsLit (x: AST.bitsLit): value = let x' = drop_chars x ' ' in VBits (mkBits (String.length x') (Z.of_string_base 2 x')) @@ -399,6 +402,10 @@ and prims_impure = ["ram_init"; "ram_read"; "ram_write"; "trace_memory_read"; "t (** {2 Utility functions on Values} *) (****************************************************************) +let length_bits (loc: AST.l) = function + | VBits { n; _ } | VMask { n; _ } -> n + | x -> raise (EvalError (loc, "bits or mask expected. Got " ^ pp_value x)) + let extract_bits (loc: AST.l) (x: value) (i: value) (w: value): value = VBits (prim_extract (to_bits loc x) (to_integer loc i) (to_integer loc w)) diff --git a/tests/test_asl.ml b/tests/test_asl.ml index 80c875f0..d6449f6a 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -74,7 +74,7 @@ let test_compare env () : unit = let lenv = Dis.build_env disEnv in let opcode = input_line inchan in - let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_int (int_of_string opcode))) in + let op = Z.of_string opcode in (try (* Evaluate original instruction *)