Merge remote-tracking branch 'origin/partial_eval' into cpp-backend

Conflicts: libASL/dune libASL/eval.ml libASL/utils.ml
UQ-PAC · Jul 19, 2024 · 68715e1 · 68715e1
2 parents 05bbe56 + 34cfa40
commit 68715e1
Show file tree

Hide file tree

Showing 27 changed files with 8,388 additions and 6,413 deletions.
diff --git a/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp b/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp
@@ -1,32 +1,41 @@
 #pragma once
 
-#include <string>
+#include <map>
 #include <memory>
+#include <string>
+#include <vector>
 
-namespace httplib {
+namespace httplib
+{
 class Client;
-} // namespace httplib;
+}  // namespace httplib
+
+// tuple of encoding and semantics
+using aslp_opcode_result_t = std::tuple<std::string, std::string>;
 
 class aslp_connection
 {
+  using params_t = std::multimap<std::string, std::string>;
+
+  const params_t& extra_params;
   std::unique_ptr<httplib::Client> client {nullptr};
 
 public:
-  aslp_connection(const std::string& server_addr, int server_port);
+  aslp_connection(const std::string& server_addr, int server_port, const params_t& extra_params = {});
   aslp_connection(aslp_connection&&) noexcept;
-  auto get_opcode(uint32_t opcode) -> std::string;
+  auto get_opcode(uint32_t opcode) -> aslp_opcode_result_t;
   void wait_active();
   ~aslp_connection();
 };
 
-
-
-class aslp_client {
+class aslp_client
+{
 private:
   const std::string server_addr;
   pid_t server_pid;
   int server_port;
   void shutdown();
+
 public:
   aslp_client(const aslp_client&) = delete;
   aslp_client(aslp_client&&) = delete;
@@ -40,26 +49,26 @@ class aslp_client {
       : server_pid(pid)
       , server_port(port)
       , server_addr(std::move(addr))
-  { }
+  {
+  }
 
   /**
    * Creates a new aslp_client with a managed server on
    * the default address, localhost:8000.
    */
-  std::unique_ptr<aslp_client> static start() {
+  std::unique_ptr<aslp_client> static start()
+  {
     return start("127.0.0.1", 8000);
   }
 
   /** Creates a new managed aslp_client with the given address and port. */
-  auto static start(const std::string& addr, int server_port) -> std::unique_ptr<aslp_client>;
+  auto static start(const std::string& addr,
+                    int server_port) -> std::unique_ptr<aslp_client>;
 
-  /** Returns the semantics for the given opcode, as a newline-separated string. */
-  auto get_opcode(uint32_t opcode) -> std::string;
+  /** Returns the semantics for the given opcode, as a newline-separated string.
+   */
+  auto get_opcode(uint32_t opcode) -> aslp_opcode_result_t;
 
   /** Destroys the aslp_client and terminates the managed server as well. */
-  virtual ~aslp_client() {
-    shutdown();
-  };
-
+  virtual ~aslp_client() { shutdown(); };
 };
-
diff --git a/aslp-cpp/source/aslp-cpp.cpp b/aslp-cpp/source/aslp-cpp.cpp
@@ -147,11 +147,14 @@ void aslp_connection::wait_active()
   std::cout << "\n";
 }
 
-std::string aslp_connection::get_opcode(uint32_t opcode)
+aslp_opcode_result_t aslp_connection::get_opcode(uint32_t opcode)
 {
   auto codestr = std::format("{:#x}", opcode);
   std::cout << codestr << "\n";
-  const auto params = httplib::Params({{"opcode", codestr}});
+  auto params = httplib::Params({{"opcode", codestr}});
+  for (const auto& pair : extra_params) {
+    params.insert(pair);
+  }
   auto req = client->Get("/", params, httplib::Headers());
 
   if (req.error() != httplib::Error::Success) {
@@ -167,19 +170,23 @@ std::string aslp_connection::get_opcode(uint32_t opcode)
   if (!result.contains("semantics")) {
     throw std::runtime_error("semantics missing");
   }
-  return result["semantics"];
+  if (!result.contains("encoding")) {
+    throw std::runtime_error("encoding name missing");
+  }
+  return {result["encoding"], result["semantics"]};
 }
 
 aslp_connection::aslp_connection(const std::string& server_addr,
-                                 int server_port)
-{
-  client = std::make_unique<httplib::Client>(server_addr, server_port);
-}
+                                 int server_port,
+                                 const params_t& extra_params) :
+  extra_params{extra_params},
+  client{std::make_unique<httplib::Client>(server_addr, server_port)}
+{}
 
 aslp_connection::aslp_connection(aslp_connection&&) noexcept = default;
 aslp_connection::~aslp_connection() = default;
 
-std::string aslp_client::get_opcode(uint32_t opcode)
+aslp_opcode_result_t aslp_client::get_opcode(uint32_t opcode)
 {
   aslp_connection conn {server_addr, server_port};
   conn.wait_active();

diff --git a/aslp-cpp/test/source/aslp-cpp_test.cpp b/aslp-cpp/test/source/aslp-cpp_test.cpp
@@ -8,7 +8,8 @@ auto main() -> int
   auto s = aslp_client::start();
 
   try {
-    auto c = s->get_opcode(0xFD430091);
+    std::string c;
+    std::tie(std::ignore, c) = s->get_opcode(0xFD430091);
     std::cout << c << "\n";
   } catch (std::runtime_error &e) {
     std::cout << " error " << e.what() << "\n";

diff --git a/bin/asli.ml b/bin/asli.ml
@@ -60,14 +60,6 @@ let gen_backends = [
     ("cpp",   (Cpu.Cpp, "offlineASL-cpp/subprojects/aslp-lifter"));
 ]
 
-let flags = [
-    ("trace:write", Eval.trace_write);
-    ("trace:fun",   Eval.trace_funcall);
-    ("trace:prim",  Eval.trace_primop);
-    ("trace:instr", Eval.trace_instruction);
-    ("eval:concrete_unknown", Value.concrete_unknown)
-]
-
 let () = Random.self_init ()
 
 let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0: string): unit =
@@ -127,7 +119,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); *)
@@ -165,7 +157,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
     | [":help"] | [":?"] ->
         List.iter print_endline help_msg;
         print_endline "\nFlags:";
-        List.iter (fun (nm, v) -> Printf.printf "  %s%s\n" (if !v then "+" else "-") nm) flags
+        Flags.StringMap.iter (fun nm v -> Printf.printf "  %s%s\n" (if v then "+" else "-") nm) (Flags.get_flags ())
     | [":opcode"; iset; opcode] ->
         (* todo: make this code more robust *)
         let op = Z.of_string opcode in
@@ -197,7 +189,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
@@ -227,9 +219,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;
@@ -238,16 +229,8 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
         close_out chan
     | (":set" :: "impdef" :: rest) ->
         Eval.set_impdef tcenv cpu.env fname rest
-    | [":set"; flag] when Utils.startswith flag "+" ->
-        (match List.assoc_opt (Utils.stringDrop 1 flag) flags with
-        | None -> Printf.printf "Unknown flag %s\n" flag;
-        | Some f -> f := true
-        )
-    | [":set"; flag] when Utils.startswith flag "-" ->
-        (match List.assoc_opt (Utils.stringDrop 1 flag) flags with
-        | None -> Printf.printf "Unknown flag %s\n" flag;
-        | Some f -> f := false
-        )
+    | [":set"; flag] ->
+        Flags.set_flag flag
     | [":project"; prj] ->
         let inchan = open_in prj in
         (try
@@ -314,6 +297,7 @@ let options = Arg.align ([
     ( "--export-aarch64", Arg.Set_string opt_export_aarch64_dir,  "       Export bundled AArch64 MRA to the given directory");
     ( "--version", Arg.Set opt_print_version, "       Print version");
     ( "--prelude", Arg.Set_string opt_prelude,"       ASL prelude file (default: ./prelude.asl)");
+    ( "--flag", Arg.String Flags.set_flag,          "       Behaviour flags to set (+) or unset (-)");
 ] )
 
 let version = "ASL 0.2.0 alpha"

diff --git 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/bin/server.ml b/bin/server.ml
@@ -17,24 +17,27 @@ open Lwt
 
 let persistent_env = lazy (Option.get (Arm_env.aarch64_evaluation_environment ()))
 
-let eval_instr (opcode: string) : string =
+let eval_instr (opcode: string) : string * string =
     let pp_raw stmt : string = Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt) |> String.trim  in
-    let address = None                                     in
-    let env' = Lazy.force persistent_env                    in
-    let stmts : Asl_ast.stmt list  = Dis.retrieveDisassembly ?address env' (Dis.build_env env') opcode in
-    let stmts'   = List.map pp_raw stmts                                                 in
-    String.concat "\n" stmts'
+    let _address = None in
 
+    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 stmts'   = List.map pp_raw stmts in
+    enc, String.concat "\n" stmts'
 
 let get_reply (jsonin: string) : Cohttp.Code.status_code * string =
   (*let json  = Yojson.Safe.from_string jsonin in *)
   let make_reply code tail =
-    (code, Yojson.Safe.to_string (`Assoc [("instruction", `String jsonin); tail])) in
+    (code, Yojson.Safe.to_string (`Assoc (["instruction", `String jsonin] @ tail))) in
   Printf.printf "Disassembling '%s'\n" jsonin;
   flush stdout;
   match (eval_instr jsonin) with
-  | exception e -> make_reply `Internal_server_error ("error", `String (Printexc.to_string e))
-  | x -> make_reply `OK ("semantics", `String x)
+  | exception e -> make_reply `Internal_server_error ["error", `String (Printexc.to_string e)]
+  | enc, x -> make_reply `OK [ "encoding", `String enc; "semantics", `String x; ]
 
 
 let unsupp_method_resp : Cohttp.Code.status_code * string =
@@ -43,26 +46,37 @@ let unsupp_method_resp : Cohttp.Code.status_code * string =
 let missing_param : Cohttp.Code.status_code * string =
   (`Bad_request, Yojson.Safe.to_string (`Assoc [("error", `String "missing opcode param.")]))
 
-(*let () = ignore (List.map (fun (f: string) -> print_endline (eval_instr f)) (tl (to_list Sys.argv))) *)
-
+let try_set_flags xs : (unit, Cohttp.Code.status_code * string) Result.t =
+  match (List.iter Flags.set_flag xs) with
+  | exception (Arg.Bad _ as e) -> Result.error (`Bad_request, Yojson.Safe.to_string (`Assoc [("error", `String (Printexc.to_string e))]))
+  | _ -> Result.ok ()
 
 let get_resp (opcode: string) : Cohttp.Code.status_code * string =
     get_reply opcode
 
 let server addr port =
   Printf.printf "Started aslp-server at http://%s:%d\n" addr port;
   flush stdout;
+
+  let oldflags = Flags.get_flags () in
+
   let callback _conn req body =
     let uri = req |> Request.uri in
     let _meth = req |> Request.meth |> Code.string_of_method in
     let _headers = req |> Request.headers |> Header.to_string in
     let body' = body |> Cohttp_lwt.Body.to_string in
-    let resp' =
-      match (Request.meth req, Uri.get_query_param uri "opcode") with
-      | `POST, _ -> body' >|= get_resp
-      | `GET, Some param -> Lwt.return (get_resp param)
-      | `GET, None -> Lwt.return missing_param
-      |  _ -> Lwt.return unsupp_method_resp
+
+    Flags.set_flags oldflags;
+
+    let resp' = 
+      match (Option.map try_set_flags (Uri.get_query_param' uri "flags")) with
+      | Some (Error xs) -> Lwt.return xs
+      | Some (Ok ()) | None ->
+        match (Request.meth req, Uri.get_query_param uri "opcode") with
+        | `POST, _ -> body' >|= get_resp
+        | `GET, Some param -> Lwt.return (get_resp param)
+        | `GET, None -> Lwt.return missing_param
+        |  _ -> Lwt.return unsupp_method_resp
     in
     resp' >>= fun (code, body) -> Server.respond_string ~status:code ~body ()
   in

diff --git a/libASL/Semantics.g4 b/libASL/Semantics.g4
@@ -46,7 +46,7 @@ type_register_slices:
 
 type:
   'Type_Bits' OPEN_PAREN expr CLOSE_PAREN  # TypeBits
-  | 'Type_Constructor(boolean)'            # TypeBoolean
+  | 'Type_Constructor("boolean")'            # TypeBoolean
   | 'Type_Constructor(' ident ')'       # TypeConstructor
   | 'Type_Register' OPEN_PAREN QUOTE width=integer QUOTE type_register_slices CLOSE_PAREN # TypeRegister
 ;

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