ocaml backend fixes for pc, export offline lifter library (#120)

* 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`. * make `dune build` build just asli the install dependency was requiring a build of all packages. note, to install asli only, you will have to use `dune install -p asli` * make `dune build offlineASL` build all aslp offline things this will also build asli if needed for the offline generation * readme: recommend dune to install package, clarify subpackages * separate offline lifter with pc support * offline depend on stage0 - Moves Primops, Value and Symbolic into stage0 to support this - Some fixes for the previous commit * update offline dune files * fix bin/dune * fix test action coverage * add js lib * ci: try to fake DUNE_INSTALL_PREFIX * readme: add alias for building all offline things * bootstrapping for offline dune files * tests: add package restrictions * reword readme --------- Co-authored-by: rina <[email protected]>
UQ-PAC · Feb 4, 2025 · 52726c4 · 52726c4
1 parent 9b487c6
commit 52726c4
Show file tree

Hide file tree

Showing 33 changed files with 1,888 additions and 100 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -3,7 +3,7 @@ name: Test partial eval
 on:
   push:
     branches:
-      - partial_eval 
+      - partial_eval
   pull_request:
     types: []
   workflow_dispatch:
@@ -45,17 +45,29 @@ jobs:
 
   offline:
     runs-on: ubuntu-latest
+    env:
+      PREFIX: /tmp/prefix
+      DUNE_INSTALL_PREFIX: /tmp/prefix
 
     steps:
     - uses: actions/checkout@v4
 
     - uses: cachix/install-nix-action@v25
-    - run: echo 'preparing nix shell environment'
 
-    - run: dune build --profile release -j4
-    - run: echo ':gen A64 aarch64_* ocaml false offlineASL' | OCAMLRUNPARAM=b dune exec asli
+    - run: |
+        echo 'preparing nix shell environment'
+        set -u
+        mkdir -p "$DUNE_INSTALL_PREFIX"
+        # echo "OCAMLPATH=$DUNE_INSTALL_PREFIX/lib:$OCAMLPATH" | tee -a "$GITHUB_ENV"
+        # ^ note: the nix shell would override this external variable
+
+    - run: dune build -p asli -j4 --profile=release
+
+    - run: dune install -p asli --profile=release
+
+    - run: 'OCAMLPATH=$PREFIX/lib:$OCAMLPATH PATH=$PREFIX/bin:$PATH dune build -p aslp_offline -j4'
 
-    - run: dune build offlineASL -j4
+    - run: dune install -p aslp_offline
 
     - run: dune build @offline-coverage -j4
 

diff --git a/README.md b/README.md
@@ -1,9 +1,9 @@
 # *ASLp* - ASL Partial Evaluator
 
-This forks ASLi to extract usable semantics from the 
-architecture specifications. 
-The semantics produced are in ASL but are reduced to contain 
-only simple control flow and scalar types, 
+This forks ASLi to extract usable semantics from the
+architecture specifications.
+The semantics produced are in ASL but are reduced to contain
+only simple control flow and scalar types,
 for use in further static analysis.
 
 ## Introduction
@@ -29,10 +29,10 @@ To build and run the ASL interpreter, you will need:
       * odoc      - OCaml documentation generator (optional)
       * dune      - OCaml build system
       * menhir    - parser generator tool
-      * ott       - tool for defining language grammars and semantics 
+      * ott       - tool for defining language grammars and semantics
       * linenoise - OCaml line editing library
       * pprint    - OCaml pretty-printing library
-      * z3        - OCaml bindings for the Z3 SMT solver 
+      * z3        - OCaml bindings for the Z3 SMT solver
       * zarith    - OCaml multiprecision arithmetic library
 
 
@@ -144,11 +144,28 @@ these steps will install the package in a location discoverable by opam and dune
 
 After installing dependencies and testing the build, run these commands in this directory:
 ```
-    opam pin . -k path
-    opam install .
+    dune build
+    dune install -p asli
 ```
 Once complete, you can verify the package is installed by running `ocamlfind query asli`.
 
+#### ASLp Offline OCaml lifter
+
+If you want to simultaneously build ASLp and use this version to generate the lifter,
+use `dune build @offline`.
+Be aware that this might re-use a cached offline lifter, even if ASLp code has changed.
+To clean the cached lifters, use `rm -v ./_build/default/*/marshalled-offline-lifter-*`.
+
+To build the offline lifter using previously compiled asli (e.g. as installed through `opam pin` as above),
+Then, use:
+```bash
+dune build -p aslp_offline
+dune install -p aslp_offline
+```
+Note: this uses the _installed_ copy of ASLp to generate the offline lifter.
+Basically, `-p` acts as if all packages other than the one listed
+do not exist in this dune project, forcing it to look elsewhere.
+This can be useful when building and installing packages individually.
 
 ### Using ASL lexer
 
@@ -206,7 +223,7 @@ ASLi>
 ```
 LLVM can be used to obtain the bytecode for a particular instruction mnemonic:
 ```bash
-$ echo 'add x1, x2, x3, LSL 4' | 
+$ echo 'add x1, x2, x3, LSL 4' |
     clang -x assembler -target aarch64 - -c -o/dev/stdout |
     llvm-objdump - -d --section=.text |
     tail -n1
@@ -274,12 +291,12 @@ For the coverage tests, the tests are simple diff tests against an expected outp
 In both cases, dune will report test failures as a difference against the expected output.
 [`dune promote`](https://dune.readthedocs.io/en/latest/concepts/promotion.html)
 can be used to update the expected files with the output from the latest run.
- 
+
 #### Differential testing
 
 The `:coverage` command is used to test equivalence of the partial evaluator and the interpreter.
 It takes a regular expression of an instruction group, then generates and evaluates the partially evaluated
-ASL as well as the original ASL and compares the final states. 
+ASL as well as the original ASL and compares the final states.
 Instruction groups can be found in the [mra_tools/arch/arch_instrs.asl](mra_tools/arch/arch_instrs.asl) file.
 ```
 ASLi> :coverage A64 aarch64_integer.+
@@ -295,7 +312,7 @@ ASLi> :coverage A64 aarch64_integer.+
 [...]
 ```
 
-"OK" indicates the machine state after both executions are the same, 
+"OK" indicates the machine state after both executions are the same,
 as we would expect if the partial evaluation is correct.
 UNDEFINED means that particular bytecode is an undefined case in the architecture.
 If an exception occurs somewhere else in the process, that will be reported as well.
@@ -304,9 +321,9 @@ If an exception occurs somewhere else in the process, that will be reported as w
 
 - Lam, K., & Coughlin, N. (2023).
 Lift-off: Trustworthy ARMv8 semantics from formal specifications.
-In A. Nadel & K. Y. Rozier (Eds.), 
+In A. Nadel & K. Y. Rozier (Eds.),
 _Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023_
-(pp. 274–283). 
+(pp. 274–283).
 TU Wien Academic Press.
 [10.34727/2023/isbn.978-3-85448-060-0_36](https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_36)
 

diff --git a/asli.opam b/asli.opam
@@ -10,13 +10,13 @@ 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"}
+  "dune" {>= "2.9"}
   "ocaml" {>= "4.14"}
   "menhir" {build}
   "ott" {build & >= "0.31"}
@@ -41,9 +41,11 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/alastairreid/asl-interpreter.git"
+dev-repo: "git+https://github.com/UQ-PAC/aslp.git"
diff --git a/aslp_offline.opam b/aslp_offline.opam
@@ -0,0 +1,33 @@
+# 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.9"}
+  "ocaml" {>= "4.14"}
+  "asli"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/UQ-PAC/aslp.git"
diff --git a/aslp_offline_jsoo.opam b/aslp_offline_jsoo.opam
@@ -0,0 +1,37 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.2.0"
+synopsis: "AArch64 Offline lifter javascript library"
+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.9"}
+  "ocaml" {>= "4.14"}
+  "aslp_offline"
+  "asli"
+  "js_of_ocaml"
+  "js_of_ocaml-ppx"
+  "zarith_stubs_js"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/UQ-PAC/aslp.git"
diff --git a/bin/asli.ml b/bin/asli.ml
@@ -42,7 +42,7 @@ let help_msg = [
     {|: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|};
     {|:gen <instr-set> <regex>       Generate an offline lifter using the given backend|};
-    {|      [pc-option] [backend] [dir]|};
+    {|      [backend] [pc-option] [dir]|};
     {|:project <file>                Execute ASLi commands in <file>|};
     {|:q :quit                       Exit the interpreter|};
     {|:run                           Execute instructions|};
@@ -199,8 +199,8 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
             (Dis.dis_decode_entry cpu.env cpu.denv decoder op);
         Option.iter close_out chan_opt
     | ":gen" :: iset :: id :: rest when List.length rest <= 3 ->
-        let pc_option = Option.value List.(nth_opt rest 1) ~default:"false" in
         let backend_str = Option.value List.(nth_opt rest 0) ~default:"ocaml" in
+        let pc_option = Option.value List.(nth_opt rest 1) ~default:"false" in
         Printf.printf "Generating lifter for %s %s with pc option %s using %s backend\n" iset id pc_option backend_str;
 
         let pc_option = match String.lowercase_ascii pc_option with

diff --git a/bin/dune b/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,15 +38,28 @@
 (executable
  (name offline_coverage)
  (public_name asloff-coverage)
+ (package aslp_offline)
  (modes exe)
  (modules offline_coverage)
  (flags (-cclib -lstdc++))
- (libraries asli.libASL offlineASL))
+ (libraries asli.libASL aslp_offline.aarch64))
 
 (executable
  (name offline_sem)
  (public_name asloff-sem)
+ (package aslp_offline)
  (modes exe)
  (modules offline_sem)
  (flags (-cclib -lstdc++))
- (libraries asli.libASL offlineASL))
+ (libraries asli.libASL aslp_offline.aarch64 aslp_offline.pc_aarch64))
+
+
+(executable
+ (name offline_js)
+ (modes js)
+ (modules offline_js)
+ (libraries asli.libASL-stage0 aslp_offline.aarch64 
+  zarith_stubs_js
+ )
+ (preprocess (pps js_of_ocaml-ppx))
+)
diff --git a/bin/offline_coverage.ml b/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  bv in
     Result.Ok stmts
   with
     | e -> Result.Error (Op_DisFail e)

diff --git a/bin/offline_js.ml b/bin/offline_js.ml
@@ -0,0 +1,22 @@
+open LibASL_stage0
+open Asl_utils
+open Asl_ast
+open Js_of_ocaml
+
+let dis (opcode: string) : stmt list =
+  let op = Z.of_string opcode in
+  let bv = Primops.prim_cvt_int_bits (Z.of_int 32) op in
+  OfflineASL.Offline.run  bv
+
+
+(*
+import("offline_js.bc.js");
+offlineLifter.dis(opcode);
+*)
+
+let () =  Js.export "offlineLifter"
+    begin object%js
+      method dis x = List.map (fun s -> pp_stmt s |> Js.string) (dis (Js.to_string x))
+    end end
+
+
diff --git a/bin/offline_sem.ml b/bin/offline_sem.ml
@@ -2,14 +2,19 @@ open LibASL
 open Asl_ast
 open Asl_utils
 
-let run (opcode: string) =
+let run (opcode: string) (pc: int option) =
   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
+  let stmts = match pc with 
+    | None -> OfflineASL.Offline.run  bv 
+    | Some x -> OfflineASL_pc.Offline.run ~pc:x bv in
   List.iter (fun s -> Printf.printf "%s\n" (pp_stmt s)) stmts
 
 let opt_instr = ref []
-let options = Arg.align ([])
+let opt_pc = ref (-1) 
+let options = Arg.align ([
+    ( "--pc", Arg.Set_int opt_pc , "set program counter (does nothing if lifter generated does not support it)");
+])
 let usage_msg = ""
 
 let _ =
@@ -18,6 +23,7 @@ let _ =
     usage_msg
 
 let main () = 
-  List.map (fun instr -> run instr) !opt_instr
+  let pc = if (!opt_pc <> -1) then Some !opt_pc else None in
+  List.map (fun instr -> run instr pc) !opt_instr 
 
 let _ = main()
diff --git a/bin/server.ml b/bin/server.ml
@@ -33,8 +33,6 @@ 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
-  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)]
   | enc, x -> make_reply `OK [ "encoding", `String enc; "semantics", `String x; ]