ocaml backend fixes for pc, export offline lifter library

.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
 

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,29 @@ 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
+
+To build the offline lifter, which depends on the main ASLp package, first install the ASLp
+package 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.
+If you want to simultaneously build ASLp and use this version to generate the lifter,
+use `dune build offlineASL`.
+
+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 +224,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 +292,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 +313,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 +322,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)
 

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/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

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))
+)

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)

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
+
+

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()

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; ]

dune

@@ -1,4 +1,4 @@
-(alias 
+(alias
   (name asl_files)
   (deps
     prelude.asl
@@ -22,4 +22,9 @@
 
 (alias
  (name default)
- (deps (package asli) (alias install)))
+ (deps (package asli) asli.install))
+
+
+(alias
+ (name aslp_offline_jsoo)
+ (deps (package aslp_offline_jsoo ) bin/offline_js.bc.js))

dune-project

@@ -31,12 +31,36 @@
   )
 )
 
+(package
+  (name aslp_offline)
+  (synopsis "AArch64 Offline lifter")
+  (description "" )
+  (depends
+    ("ocaml"     (>= "4.14"))
+    "asli"
+  )
+)
+
+(package
+  (name aslp_offline_jsoo)
+  (synopsis "AArch64 Offline lifter javascript library")
+  (description "" )
+  (depends
+    ("ocaml"     (>= "4.14"))
+    aslp_offline
+    asli
+    js_of_ocaml
+    js_of_ocaml-ppx
+    zarith_stubs_js
+  )
+)
+
 (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)