Initial support for symbolic opcodes

bin/asli.ml

@@ -11,6 +11,7 @@ open LibASL
 
 open Asl_ast
 open Value
+open Symbolic
 open Eval
 open Asl_utils
 
@@ -39,8 +40,8 @@ let help_msg = [
     {|:? :help                       Show this help message|};
     {|:elf <file>                    Load an ELF file|};
     {|:opcode <instr-set> <int>      Decode and execute opcode|};
-    {|:sem <instr-set> <int>         Decode and print opcode semantics|};
-    {|:ast <instr-set> <int> [file]  Decode and write opcode semantics to stdout or a file, in a structured ast format|};
+    {|:sem <instr-set> <bits>        Decode and print opcode semantics|};
+    {|:ast <instr-set> <bits> [file] Decode and write opcode semantics to stdout or a file, in a structured ast format|};
     {|:gen <instr-set> <regex>       Generate an offline lifter using the given backend|};
     {|      [backend] [pc-option] [dir]|};
     {|:project <file>                Execute ASLi commands in <file>|};
@@ -186,17 +187,16 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
         ) encodings;
     | [":sem"; iset; opcode] ->
         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
+        Printf.printf "Decoding instruction %s %s\n" iset opcode;
+        cpu'.sem iset opcode
     | ":ast" :: iset :: opcode :: rest when List.length rest <= 1 ->
-        let op = Z.of_string opcode in
+        let op = sym_bits_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
         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_sym cpu.env cpu.denv decoder op);
         Option.iter close_out chan_opt
     | ":gen" :: iset :: id :: rest when List.length rest <= 3 ->
         let backend_str = Option.value List.(nth_opt rest 0) ~default:"ocaml" in

libASL/cpu.ml

@@ -8,6 +8,7 @@
 module AST = Asl_ast
 
 open Asl_utils
+open Symbolic
 
 type gen_backend =
     | Ocaml
@@ -25,7 +26,7 @@ type cpu = {
     setPC    : Primops.bigint -> unit;
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
-    sem      : string -> Primops.bigint -> unit;
+    sem      : string -> string -> unit;
     gen      : string -> string -> bool -> gen_backend -> string -> unit;
 }
 
@@ -55,12 +56,16 @@ 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 (iset: string) (opcode: string): unit =
         let decoder = Eval.Env.getDecoder env (Ident iset) in
+
+        (* Parse symbolic opcode *)
+        let op = sym_bits_of_string opcode in
+
         List.iter
             (fun s -> Printf.printf "%s\n" (pp_stmt s))
-            (Dis.dis_decode_entry env denv decoder opcode)
-
+            (Dis.dis_decode_entry_sym env denv decoder op)
+        
     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);
 

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      : string -> string -> unit;
     gen      : string -> string -> bool -> gen_backend -> string -> unit;
 }
 

libASL/dis.ml

@@ -14,7 +14,6 @@ module TC   = Tcheck
 open AST
 open Asl_utils
 open Value
-
 open Symbolic
 
 module StringCmp = struct
@@ -1417,53 +1416,64 @@ and dis_stmt' (x: AST.stmt): unit rws =
         DisEnv.write [Stmt_Assert(expr_false, loc)]
     )
 
-let dis_encoding (x: encoding) (op: Primops.bigint): (stmt list option) rws =
+let dis_encoding (x: encoding) (op: sym): (stmt list option) 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); *)
-    match Eval.eval_opcode_guard loc opcode op with
-    | Some op ->
+    let ok = (match opcode with
+    | Opcode_Bits b -> sym_eq     loc op (Val (from_bitsLit b))
+    | Opcode_Mask m -> sym_inmask loc op (to_mask loc (from_maskLit m))
+    ) in
+    if (bool_of_sym ok) then begin
         if !Eval.trace_instruction then Printf.printf "TRACE: instruction %s\n" (pprint_ident nm);
 
         let@ () = DisEnv.traverse_ (function (IField_Field (f, lo, wd)) ->
-            let v = extract_bits' loc op lo wd in
-            if !Eval.trace_instruction then Printf.printf "      %s = %s\n" (pprint_ident f) (pp_value v);
-            declare_assign_var Unknown (val_type v) f (Val v)
+            let s = sym_extract_bits loc op (sym_of_int lo) (sym_of_int wd) in
+            if !Eval.trace_instruction then Printf.printf "      %s = %s\n" (pprint_ident f) (pp_sym s);
+            declare_assign_var Unknown (sym_type s) f s
         ) fields in
 
         let@ guard' = dis_expr loc guard in
         if to_bool loc (sym_value_unsafe guard') then begin
             List.iter (fun (i, b) ->
-                if eval_eq loc (extract_bits' loc op i 1) (from_bitsLit b) then
+                if eval_eq loc (sym_value_unsafe (sym_extract_bits loc op (sym_of_int i) (sym_of_int 1))) (from_bitsLit b) then
                     raise (Throw (loc, Exc_Unpredictable))
             ) unpreds;
             (* dis_encoding: we cannot guarantee that these statements are fully evaluated. *)
             DisEnv.pure (Some b)
         end else begin
             DisEnv.pure None
         end
-    | None -> DisEnv.pure None
-
-let dis_decode_slice (loc: l) (x: decode_slice) (op: Primops.bigint): value rws =
+    end else begin
+        DisEnv.pure None
+    end
+
+let rec dis_decode_pattern (loc: AST.l) (x: decode_pattern) (op: sym): sym =
+    match x with
+    | DecoderPattern_Bits     b -> sym_eq     loc op (Val (from_bitsLit b))
+    | DecoderPattern_Mask     m -> sym_inmask loc op (to_mask loc (from_maskLit m))
+    | DecoderPattern_Wildcard _ -> sym_true
+    | DecoderPattern_Not      p -> sym_not_bool loc (dis_decode_pattern loc p op)
+
+let dis_decode_slice (loc: l) (x: decode_slice) (op: sym): sym 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
+        (*let op = Value.from_bitsInt (lo+wd) op in*)
+        DisEnv.pure @@ sym_extract_bits loc op (sym_of_int lo) (sym_of_int wd)
     | DecoderSlice_FieldName f ->
-        (* assumes expression always evaluates to concrete value. *)
-        let+ _,f' = DisEnv.getVar loc f in sym_value_unsafe f'
+        let+ _,f' = DisEnv.getVar loc f in f'
     | DecoderSlice_Concat fs ->
         (* assumes expression always evaluates to concrete value. *)
         let+ fs' = DisEnv.traverse (DisEnv.getVar loc) fs in
-        eval_concat loc (List.map (fun (_,s) -> sym_value_unsafe s) fs')
+        sym_concat loc (List.map (fun (t,s) -> (width_of_type loc t, s)) fs')
     )
 
 (* Duplicate of eval_decode_case modified to print rather than eval *)
-let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: Primops.bigint): string rws =
+let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: sym): string 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) Fun.id body
-and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): string rws =
+and dis_decode_case' (loc: AST.l) (x: decode_case) (op: sym): string rws =
     (match x with
     | DecoderCase_Case (ss, alts, loc) ->
             let@ vs = DisEnv.traverse (fun s -> dis_decode_slice loc s op) ss in
@@ -1482,12 +1492,12 @@ and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): string
     )
 
 (* Duplicate of eval_decode_alt modified to print rather than eval *)
-and dis_decode_alt (loc: l) (x: decode_alt) (vs: value list) (op: Primops.bigint): string option rws =
-    let body = dis_decode_alt' loc x vs op in
+and dis_decode_alt (loc: l) (x: decode_alt) (ss: sym list) (op: sym): string option rws =
+    let body = dis_decode_alt' loc x ss op in
     if no_debug() then body
     else DisEnv.scope loc "dis_decode_alt" (pp_decode_alt x) Option.(fold ~none:"(unmatched)" ~some:Fun.id) body
-and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): string option rws =
-    if List.for_all2 (Eval.eval_decode_pattern loc) ps vs then
+and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (ss: sym list) (op: sym): string option rws =
+    if List.for_all2 (fun p s -> (bool_of_sym (dis_decode_pattern loc p s))) ps ss then
         (match b with
         | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable))
         | DecoderBody_UNALLOC loc -> raise (Throw (loc, Exc_Undefined))
@@ -1529,9 +1539,8 @@ 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)
+                    let s = sym_extract_bits loc op (sym_of_int lo) (sym_of_int wd) in
+                    declare_assign_var loc (sym_type s) f s
                 ) fs
                 in
                 let@ result = dis_decode_case loc c op in
@@ -1553,10 +1562,15 @@ let enum_types env i =
     | _ -> None
 
 (* Actually perform dis *)
-let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list =
+let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: sym_bits): string * stmt list =
     let DecoderCase_Case (_,_,loc) = decode in
-    let lenv = {lenv with trace = ["dis_core", "0x" ^ Z.format "%08x" op, Unknown]} in
-    let (enc,lenv',stmts) = (dis_decode_case loc decode op) config lenv in
+
+    (* Declare symbolic fields as globals *)
+    let fields = fields_of_sym_bits op in
+    let field_names = List.map fst fields in
+    let globals = List.fold_left (fun idents name -> IdentSet.add name idents) globals field_names in
+
+    let (enc,lenv',stmts) = (dis_decode_case loc decode (sym_of_sym_bits 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
     (* List.iter (fun (v,t) -> Printf.printf ("%s:%s\n") v (pp_type t)) varentries; *)
@@ -1566,7 +1580,7 @@ let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: P
     let stmts' = Transforms.FixRedefinitions.run (globals : IdentSet.t) 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.CommonSubExprElim.do_transform stmts' globals in
     let stmts' = Transforms.CopyProp.copyProp stmts' in
     let stmts' = Transforms.RedundantSlice.do_transform bindings stmts' in
     let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in
@@ -1591,7 +1605,7 @@ let dis_core ~(config:config) ((lenv,globals): env) (decode: decode_case) (op: P
    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) (op: sym_bits): 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
   let stmts = match !Symbolic.use_vectoriser with
@@ -1605,9 +1619,12 @@ let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode:
         RASL_check.AllowedLanguageConstructs.check_stmts_exc (snd stmts);
     stmts
 
-let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list =
+let dis_decode_entry_sym (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: sym_bits): stmt list =
   snd @@ dis_decode_entry_with_inst env (lenv,globals) decode op
 
+let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list =
+    dis_decode_entry_sym env (lenv,globals) decode (sym_bits_of_bv (Primops.prim_cvt_int_bits (Z.of_int 32) op))
+
 let build_env (env: Eval.Env.t): env =
     let env = Eval.Env.freeze env in
     let lenv = LocalEnv.init env in
@@ -1655,4 +1672,5 @@ 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 (Z.of_string opcode)
+    let op = sym_bits_of_string opcode in
+    dis_decode_entry_sym env lenv decoder op