Merge pull request #55 from UQ-PAC/taint

Offline Partial Eval

bin/asli.ml

@@ -205,6 +205,10 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
             (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);
         Option.iter close_out chan_opt
+    | [":gen"; iset; id] ->
+        let cpu' = Cpu.mkCPU cpu.env cpu.denv in
+        Printf.printf "Generating lifter for %s %s\n" iset id;
+        cpu'.gen iset id
     | ":dump" :: iset :: opcode :: rest ->
         let fname = 
             (match rest with 

bin/dune

@@ -33,3 +33,18 @@
  (flags (-cclib -lstdc++))
  (libraries libASL unix))
 
+(executable
+ (name offline_coverage)
+ (public_name asloff-coverage)
+ (modes exe)
+ (modules offline_coverage)
+ (flags (-cclib -lstdc++))
+ (libraries libASL offlineASL))
+
+(executable
+ (name offline_sem)
+ (public_name asloff-sem)
+ (modes exe)
+ (modules offline_sem)
+ (flags (-cclib -lstdc++))
+ (libraries libASL offlineASL))

bin/offline_coverage.ml

@@ -0,0 +1,96 @@
+open LibASL
+open Testing
+open Asl_ast
+open Value
+
+let () = Printexc.register_printer
+    (function
+    | Value.EvalError (loc, e) ->
+        Some ("EvalError at " ^ pp_loc loc ^ ": " ^ e)
+    | _ -> None)
+
+let op_dis (op: int): stmt list opresult =
+  let bv = Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_int op) in
+  try
+    let stmts = OfflineASL.Offline.run bv in
+    Result.Ok stmts
+  with
+    | 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 initenv = Env.copy env in
+  Random.self_init ();
+  let vals = (List.init 64 (fun _ -> Z.of_int64 (Random.int64 Int64.max_int))) in
+  Eval.initializeRegistersAndMemory initenv vals;
+  Eval.initializeGlobals initenv;
+
+  let initenv = Env.freeze initenv in
+
+  let (let*) = Result.bind in
+  let* evalenv = op_eval initenv iset op' in
+  let* disstmts = op_dis op in
+  let* disevalenv = op_diseval initenv disstmts in
+  op_compare (evalenv, disevalenv)
+
+let run opt_verbose instr env =
+  let iset = "A64" in
+  let encodings = get_opcodes opt_verbose iset instr env in
+  List.iter (fun (enc, fields, opt_opcodes) ->
+      Printf.printf "\nENCODING: %s\n" enc;
+      match opt_opcodes with
+      | None -> Printf.printf "(encoding unused)\n";
+      | Some opcodes ->
+          List.iter (fun (op, valid) ->
+              let fs = fields_of_opcode fields op in
+              Printf.printf "%s: %s --> " (hex_of_int op) (pp_enc_fields fs);
+              flush stdout;
+              if valid then
+                  let result = op_test_opcode env iset op in
+                  Printf.printf "%s\n" (pp_opresult (fun _ -> "OK") result)
+              else Printf.printf "(invalid)\n";
+          ) opcodes
+  ) encodings
+
+let opt_instr = ref []
+let options = Arg.align ([])
+let usage_msg = ""
+
+let _ =
+  Arg.parse options
+    (fun s -> opt_instr := (!opt_instr) @ [s])
+    usage_msg
+
+let rec process_command tcenv env cmd =
+  match String.split_on_char ' ' cmd with
+  | (":set" :: "impdef" :: rest) ->
+        let cmd = String.concat " " rest in
+        let (x, e) = LoadASL.read_impdef tcenv Unknown cmd in
+        let v = Eval.eval_expr Unknown env e in
+        Eval.Env.setImpdef env x v
+  | [":project"; prj] ->
+      let inchan = open_in prj in
+      (try
+          while true do
+              process_command tcenv env (input_line inchan)
+          done
+      with
+      | End_of_file ->
+          close_in inchan
+      )
+  | [""] -> ()
+  | _ -> Printf.printf "Ignoring: %s\n" cmd
+
+let main () = 
+  let opt_verbose = ref false in
+  let env = match Eval.aarch64_evaluation_environment ~verbose:!opt_verbose () with
+  | Some e -> e
+  | _ -> failwith "Unable to build evaluation environment." in
+  let filenames = Option.get Eval.aarch64_asl_files in
+  let prj_files = List.filter (fun f -> Utils.endswith f ".prj") (snd filenames) in
+  let tcenv = Tcheck.Env.mkEnv Tcheck.env0 in
+  List.iter (fun f -> process_command tcenv env (":project " ^ f)) prj_files;
+  List.map (fun instr -> run opt_verbose instr env) !opt_instr
+
+let _ = ignore (main())

bin/offline_sem.ml

@@ -0,0 +1,23 @@
+open LibASL
+open Asl_ast
+open Asl_utils
+
+let run (opcode: string) =
+  let op = Z.of_string opcode in
+  let bv = Primops.prim_cvt_int_bits (Z.of_int 32) op in
+  let stmts = OfflineASL.Offline.run bv in
+  List.iter (fun s -> Printf.printf "%s\n" (pp_stmt s)) stmts
+
+let opt_instr = ref []
+let options = Arg.align ([])
+let usage_msg = ""
+
+let _ =
+  Arg.parse options
+    (fun s -> opt_instr := (!opt_instr) @ [s])
+    usage_msg
+
+let main () = 
+  List.map (fun instr -> run instr) !opt_instr
+
+let _ = main()

libASL/asl_utils.ml

@@ -32,10 +32,15 @@ let mk_bindings (xs: (ident * 'a) list): 'a Bindings.t =
 let pp_bindings (pp: 'a -> string) (bs: 'a Bindings.t): string =
     String.concat ", " (List.map (fun (k, v) -> pprint_ident k ^"->"^ pp v) (Bindings.bindings bs))
 
+let bindings_of_list (l: (ident * 'a) list): 'a Bindings.t =
+    List.fold_right (fun (k,v) -> Bindings.add k v) l Bindings.empty
 
 (** {2 Sets of identifiers} *)
 module IdentSet = Set.Make(Id)
 
+let pp_identset is =
+    String.concat ", " (List.map (fun k -> pprint_ident k) (IdentSet.elements is))
+
 (** merge a list of sets *)
 let unionSets (idss: IdentSet.t list): IdentSet.t =
     List.fold_left IdentSet.union IdentSet.empty idss
@@ -57,6 +62,8 @@ let addToBindingSet (k: ident) (v: ident) (bs: IdentSet.t Bindings.t): IdentSet.
 let to_sorted_list (s: IdentSet.t): ident list =
     IdentSet.elements s
 
+let bindings_domain (b: 'a Bindings.t): IdentSet.t =
+  Bindings.fold (fun k _ -> IdentSet.add k) b IdentSet.empty
 
 (****************************************************************)
 (** {2 Equivalence classes}                                     *)
@@ -538,6 +545,28 @@ let masklength (x: string): int =
     String.iter (function ' ' -> () | _ -> r := !r + 1) x;
     !r
 
+(****************************************************************)
+(** {2 Function signature accessors}                            *)
+(****************************************************************)
+
+let fnsig_get_rt         (a,b,c,d,e,f) = a
+let fnsig_get_typed_args (a,b,c,d,e,f) = b
+let fnsig_get_targs      (a,b,c,d,e,f) = c
+let fnsig_get_args       (a,b,c,d,e,f) = d
+let fnsig_get_body       (a,b,c,d,e,f) = f
+
+let fnsig_set_rt         (_,b,c,d,e,f) a = (a,b,c,d,e,f)
+let fnsig_set_typed_args (a,_,c,d,e,f) b = (a,b,c,d,e,f)
+let fnsig_set_targs      (a,b,_,d,e,f) c = (a,b,c,d,e,f)
+let fnsig_set_args       (a,b,c,_,e,f) d = (a,b,c,d,e,f)
+let fnsig_set_body       (a,b,c,d,e,_) f = (a,b,c,d,e,f)
+
+let fnsig_upd_rt         upd (a,b,c,d,e,f) = (upd a,b,c,d,e,f)
+let fnsig_upd_typed_args upd (a,b,c,d,e,f) = (a,upd b,c,d,e,f)
+let fnsig_upd_targs      upd (a,b,c,d,e,f) = (a,b,upd c,d,e,f)
+let fnsig_upd_args       upd (a,b,c,d,e,f) = (a,b,c,upd d,e,f)
+let fnsig_upd_body       upd (a,b,c,d,e,f) = (a,b,c,d,e,upd f)
+
 (****************************************************************
  * End
  ****************************************************************)

libASL/call_graph.ml

@@ -0,0 +1,79 @@
+open Asl_ast
+open Asl_utils
+open Asl_visitor
+open Utils
+
+type state = {
+  mutable callers : IdentSet.t Bindings.t;
+  mutable seen : IdentSet.t;
+  mutable worklist : IdentSet.t;
+}
+
+class call_visitor(fn : ident -> unit) = object (self)
+  inherit Asl_visitor.nopAslVisitor
+  method! vlexpr e =
+    (match e with
+    | LExpr_Write (f, _, _) -> fn f
+    | LExpr_ReadWrite (g, s, _, _) -> fn g; fn s
+    | _ -> ());
+    DoChildren
+  method! vexpr e =
+    (match e with
+    | Expr_TApply (f, _, _) -> fn f
+    | _ -> ());
+    DoChildren
+  method! vstmt e =
+    (match e with
+    | Stmt_TCall (f, _, _, _) -> fn f
+    | _ -> ());
+    DoChildren
+end
+
+let init_state i: state =
+  { callers = Bindings.empty; seen = i; worklist = i }
+
+let get_callers (st: state) id =
+  match Bindings.find_opt id st.callers with
+  | None -> IdentSet.empty
+  | Some v -> v
+
+let callback (st: state) (caller: ident) (callee: ident) =
+  (* Add caller edge *)
+  let existing = get_callers st callee in
+  st.callers <- Bindings.add callee (IdentSet.add caller existing) st.callers;
+  (* Add to worklist if a new callee *)
+  if not (IdentSet.mem callee st.seen) then st.worklist <- IdentSet.add callee st.worklist;
+  (* Mark as seen *)
+  st.seen <- IdentSet.add callee st.seen
+
+let get_body i env =
+  match Eval.Env.getFunOpt Unknown env i with
+  | Some fnsig -> fnsig_get_body fnsig
+  | _ -> []
+
+let run (init: IdentSet.t) frontier (env: Eval.Env.t): (IdentSet.t Bindings.t * IdentSet.t) =
+  (* create mutable state with initial worklist, seen, empty edges *)
+  let rec iter st = begin
+    (* Get fns to visit, clear worklist *)
+    let delta = st.worklist in
+    st.worklist <- IdentSet.empty;
+
+    (* Walk each function in delta *)
+    IdentSet.iter (fun fn ->
+      let walker = new call_visitor(callback st fn) in
+      let body = get_body fn env in
+      let _ = visit_stmts walker body in
+      ()) (IdentSet.diff delta frontier);
+
+    (* If more fns to process, loop *)
+    if IdentSet.cardinal st.worklist = 0 then ()
+    else iter st
+  end in
+
+  let st = init_state init in
+  let _ = iter st in
+  (* Filter seen to only include functions with implementations *)
+  let seen = IdentSet.filter (fun v -> not (isNone (Eval.Env.getFunOpt Unknown env v))) st.seen in
+  let seen = IdentSet.diff seen frontier in
+  (st.callers, seen)
+

libASL/cpu.ml

@@ -19,6 +19,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
+    gen      : string -> string -> unit
 }
 
 let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
@@ -55,6 +56,15 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
             (fun s -> Printf.printf "%s\n" (pp_stmt s))
             (Dis.dis_decode_entry env denv decoder op)
 
+    and gen (iset: string) (pat: string): unit =
+        (* Build the symbolic lifter *)
+        let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run iset pat env in
+
+        (* Build backend program *)
+        (* TODO: other backends *)
+        if not (Sys.file_exists "offlineASL") then failwith "Can't find target dir offlineASL\n";
+        Ocaml_backend.run decoder_id decoder_fnsig tests instrs "offlineASL"
+
     in
     {
         env      = env;
@@ -65,7 +75,8 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
         setPC    = setPC;
         elfwrite = elfwrite;
         opcode   = opcode;
-        sem      = sem
+        sem      = sem;
+        gen      = gen
     }
 
 (****************************************************************

libASL/cpu.mli

@@ -15,6 +15,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
+    gen      : string -> string -> unit
 }
 
 val mkCPU : Eval.Env.t -> Dis.env -> cpu