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

@@ -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;

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 ();

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);

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)

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
 
 
 (****************************************************************)

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 ();

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))
 

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 *)