new offline lifter & asli packages, make dune build offline lifter

We now define two packages, asli and aslp_offline. The offline
lifter library gets a different name depending on whether
its built with pc support which is enabled by default in
offlineASL/gen-command (breaking offline-coverage).

libASL/dune now invokes asli to generate the lifter into the
build directory. This makes everything buildable
so the offline lifter should be useable as an opam pin dependency.

Asli can generate the dune to build the offline lifter,
but there is a little bit bit of manual mess, e.g. regarding
the command to build asli. We also don't properly invalidate the
cached marshalled generated lifter (which appears in
_build/default/marshalled-offline-lifter-*) when we rebuild
asli; to regenerate the lifter you must first run `dune clean`.

asli.opam

@@ -10,11 +10,11 @@ interactive execution of ASL statements and expressions,
 executing opcodes one at a time,
 loading ELF files and executing Arm binaries.
 """
-maintainer: ["Alastair Reid <[email protected]>"]
-authors: ["Alastair Reid"]
+maintainer: ["UQ-PAC"]
+authors: ["UQ-PAC"]
 license: "BSD-3-Clause"
-homepage: "https://github.com/alastairreid/asl-interpreter"
-bug-reports: "https://github.com/alastairreid/asl-interpreter/issues"
+homepage: "https://github.com/UQ-PAC/aslp"
+bug-reports: "https://github.com/UQ-PAC/aslp/issues"
 depends: [
   "dune" {>= "2.8"}
   "ocaml" {>= "4.14"}
@@ -46,4 +46,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/alastairreid/asl-interpreter.git"
+dev-repo: "git+https://github.com/UQ-PAC/aslp.git"

aslp_offline.opam

@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.2.0"
+synopsis: "AArch64 Offline lifter"
+description: ""
+maintainer: ["UQ-PAC"]
+authors: ["UQ-PAC"]
+license: "BSD-3-Clause"
+homepage: "https://github.com/UQ-PAC/aslp"
+bug-reports: "https://github.com/UQ-PAC/aslp/issues"
+depends: [
+  "dune" {>= "2.8"}
+  "ocaml" {>= "4.14"}
+  "asli"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/UQ-PAC/aslp.git"

bin/dune

@@ -2,6 +2,7 @@
 (executable
  (name asli)
  (public_name asli)
+ (package asli)
  (modes exe byte)
  (modules asli)
  (flags (-cclib -lstdc++))
@@ -11,6 +12,7 @@
 (executable
  (name server)
  (public_name aslp-server)
+ (package asli)
  (modes exe)
  (modules server)
  (flags (-cclib -lstdc++))
@@ -36,6 +38,7 @@
 (executable
  (name offline_coverage)
  (public_name asloff-coverage)
+ (package aslp_offline)
  (modes exe)
  (modules offline_coverage)
  (flags (-cclib -lstdc++))
@@ -44,6 +47,7 @@
 (executable
  (name offline_sem)
  (public_name asloff-sem)
+ (package aslp_offline)
  (modes exe)
  (modules offline_sem)
  (flags (-cclib -lstdc++))

bin/offline_coverage.ml

@@ -12,7 +12,7 @@ let () = Printexc.register_printer
 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
+    let stmts = OfflineASL.Offline.run ~pc:0 bv in
     Result.Ok stmts
   with
     | e -> Result.Error (Op_DisFail e)

dune-project

@@ -31,12 +31,22 @@
   )
 )
 
+(package
+  (name aslp_offline)
+  (synopsis "AArch64 Offline lifter")
+  (description "" )
+  (depends
+    ("ocaml"     (>= "4.14"))
+    "asli"
+  )
+)
+
 (license BSD-3-Clause)
-(authors "Alastair Reid")
-(maintainers "Alastair Reid <[email protected]>")
-(source (github alastairreid/asl-interpreter))
-(bug_reports "https://github.com/alastairreid/asl-interpreter/issues")
-(homepage "https://github.com/alastairreid/asl-interpreter")
+(authors "UQ-PAC")
+(maintainers "UQ-PAC")
+(source (github UQ-PAC/aslp))
+(bug_reports "https://github.com/UQ-PAC/aslp/issues")
+(homepage "https://github.com/UQ-PAC/aslp")
 ; (documentation ...)
 
 (generate_opam_files true)

libASL/dune

@@ -45,7 +45,7 @@
    scala_backend 
    arm_env pretransforms flags
    )
- (preprocessor_deps (alias ../asl_files) (alias cpp_backend_files))
+ (preprocessor_deps (alias ../asl_files) (alias cpp_backend_files) ../offlineASL/template_offline_utils.ml)
  (preprocess (pps ppx_blob))
  (libraries libASL_stage0 libASL_support str mlbdd))
 

libASL/ocaml_backend.ml

@@ -343,6 +343,7 @@ let write_fn name (ret_tyo,_,targs,args,_,body) st =
 
 let init_st oc = { depth = 0; skip_seq = false; oc ; ref_vars = IdentSet.empty } 
 let global_deps = ["Offline_utils"]
+let offline_utils_file = [%blob "../offlineASL/template_offline_utils.ml"]
 
 (* Write an instruction file, containing just the behaviour of one instructions *)
 let write_instr_file fn fnsig dir =
@@ -378,30 +379,65 @@ let write_decoder_file use_pc fn fnsig deps dir =
   close_out oc;
   m 
 
+let write_new_dune_file use_pc files dir  : unit = 
+  let target_gen_files = String.concat "" @@ List.map (fun k ->
+    Printf.sprintf "    %s.ml\n" k
+  ) files in
+  let oc = open_out (dir ^ "/dune") in
+  Printf.fprintf oc "
+  (rule (targets \n%s) 
+    (deps gen-command)
+    (action (chdir %%{workspace_root} 
+    (with-stdin-from %s/gen-command (run asli))
+  )))"
+  target_gen_files dir ;
+  Printf.fprintf oc "\n\n";
+  Printf.fprintf oc "
+  (library
+    (name offlineASL)
+    (public_name aslp_offline.%s)
+    (flags
+      (:standard -w -27 -w -33 -cclib -lstdc++))
+    (modules \n"
+    (if use_pc then "pc_aarch64" else "aarch64") ;
+    List.iter (fun k ->
+      Printf.fprintf oc "    %s\n" k
+    ) (files);
+    Printf.fprintf oc "  )
+    (libraries asli.libASL))"
+
+
 (* Write the dune build file *)
 let write_dune_file use_pc files dir =
   let oc = open_out (dir ^ "/dune") in
   Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND
 (library
   (name offlineASL)
-  (public_name asli.offline)
+  (public_name aslp_offline.%s)
   (flags
     (:standard -w -27 -w -33 -cclib -lstdc++))
-  (modules \n";
+  (modules \n"
+  (if use_pc then "pc_aarch64" else "aarch64") ;
   List.iter (fun k ->
     Printf.fprintf oc "    %s\n" k
   ) files;
   Printf.fprintf oc "  )
   (libraries asli.libASL))";
   close_out oc
 
+let write_ibi dir = 
+  let oc = open_out (dir ^ "/Offline_utils.ml") in
+  output_string oc offline_utils_file ;
+  close_out oc
+
 (* Write all of the above, expecting offline_utils.ml to already be present in dir *)
 let run config dfn dfnsig tests fns =
   let dir = config.output_directory in
   let files = Bindings.fold (fun fn fnsig acc -> (write_instr_file fn fnsig dir)::acc) fns [] in
   let files = (write_test_file tests dir)::files in
   let decoder = write_decoder_file config.use_pc dfn dfnsig files dir in
-  write_dune_file config.use_pc (decoder::files@global_deps) dir
+  write_new_dune_file config.use_pc (decoder::files@global_deps) dir ;
+  write_ibi dir
 
 module OcamlBackend : Backend = struct
   let run ~(config:conf) dfn dfnsig tests fns = run config dfn dfnsig tests fns