Scala backend & lifter-optimiser bdd copyprop (#102)

* Add scala backend for BASIL

* Add lifttime PC variable

Optional support for offline lifter to specify the PC value
at lifttime.

* Remove problematic list, add missing variables

* Optional pass to remove unsupported globals

* Whitespace in transforms

* Re-enable case simp for offline

* Decoder cleanup and sanity checks

* Simplify reachability based on enc

* Add lifttime PC variable

Optional support for offline lifter to specify the PC value
at lifttime.

* Remove problematic list, add missing variables

* Optional pass to remove unsupported globals

* Whitespace in transforms

* Re-enable case simp for offline

* Decoder cleanup and sanity checks

* Simplify reachability based on enc

* wip rt copyprop

* use bdd lattice for clobbered & read

* refac

* untested xform to ternary

* not working

* refactor so analysis and transform both called into from bdd AI walk

* fix anlaysis a bit and add bvadd

* cleanup bvops

* Eliminate comparisons during IntToBits

Leverage interval information to reduce trivial comparisons
during post-passes, then cleanup in RemoveUnused.

* fix rebuild expr

* passing cov disabled

* test and fix bdd sle/slt

* Merged backends (#80)

* Add scala backend for BASIL

* Add C++ Backend for LLVM 

* add aslBackwardsVisitor

* aslVisitor: change vstmt to return stmt list

BREAKING!
This change affects the signature of the Asl_visitor.visit_stmt method.
For compatibility, a visit_stmt_single method is provided with
equivalent behaviour to the old visit_stmt. There is also an added
helper function to convert visitActions on single statements to
visitActions on a list of statements.

Both of these compatibility helpers WILL THROW if used with a visitor
that returns non-singleton statement lists.

This gives the user the flexibility to insert new statements or delete
statements entirely. On the other hand, post-functions in
ChangeDoChildrenPost will need to handle lists of functions as well.

This follows the original CIL visitor: https://people.eecs.berkeley.edu/~necula/cil/api/Cil.cilVisitor.html

* fix backwards visitor and rearrange code

it is no longer a good idea for the backwards and forwards visitors to have a subtyping relation.

* support -x 0 to print encoding name. (#78)

this is very useful when looking for the name of an encoding,
without cluttering the output with the disassembly trace.

the default debug_level has been lowered to -1 to support -x 0
as a non-default level. we cannot print by default since that
would clutter stdout when used as a library.



Co-authored-by: rina <[email protected]>

* progress

* possibly working

* build standalone

* print lifted semantics

* readme

* add mill script

* add generic lifter interface

* delete old utils

* generate separate scala assembly file

* cleanup

* update tests

* marshall offline lifter

* fix symbolic lifter merge

* update action

* update cpp lifter

* cpp: allow llvm 18

* cpp: clean up offlineASL-cpp folder

delete old hpp files in root

reset meson.build to empty

---------

Co-authored-by: Nicholas Coughlin <[email protected]>
Co-authored-by: rina <[email protected]>

.github/workflows/test.yml

@@ -53,7 +53,7 @@ jobs:
     - run: echo 'preparing nix shell environment'
 
     - run: dune build --profile release -j4
-    - run: echo ':gen A64 aarch64_* ocaml offlineASL' | OCAMLRUNPARAM=b dune exec asli
+    - run: echo ':gen A64 aarch64_* ocaml false offlineASL' | OCAMLRUNPARAM=b dune exec asli
 
     - run: dune build offlineASL -j4
 

.gitignore

@@ -24,3 +24,8 @@ scripts/total.txt
 build/
 
 offlineASL/aarch64_*
+offlineASL-cpp/subprojects/aslp-lifter/src/generated/*
+offlineASL-cpp/subprojects/aslp-lifter/include/aslp/generated/*
+
+
+

asli.opam

@@ -29,6 +29,7 @@ depends: [
   "lwt"
   "cohttp-lwt-unix"
   "yojson"
+  "mlbdd"
   "odoc" {with-doc}
 ]
 build: [

bin/asli.ml

@@ -27,7 +27,10 @@ let opt_export_aarch64_dir = ref ""
 let opt_verbose = ref false
 
 
-let () = Printexc.register_printer
+
+let () = 
+    Printexc.record_backtrace true ;
+    Printexc.register_printer
     (function
     | Value.EvalError (loc, msg) ->
         Some (Printf.sprintf "EvalError at %s: %s" (pp_loc loc) msg)
@@ -40,7 +43,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|};
-    {|      [backend] [dir]|};
+    {|      [pc-option] [backend] [dir]|};
     {|:project <file>                Execute ASLi commands in <file>|};
     {|:q :quit                       Exit the interpreter|};
     {|:run                           Execute instructions|};
@@ -56,6 +59,7 @@ let help_msg = [
 
 (** supported backends for :gen and their default output directories *)
 let gen_backends = [
+    ("scala", (Cpu.Scala, "offlineASL-scala/lifter/src/generated"));
     ("ocaml", (Cpu.Ocaml, "offlineASL"));
     ("cpp",   (Cpu.Cpp, "offlineASL-cpp/subprojects/aslp-lifter"));
 ]
@@ -197,18 +201,24 @@ 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 :: rest when List.length rest <= 2 ->
+    | ":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
-        Printf.printf "Generating lifter for %s %s using %s backend\n" iset id backend_str;
+        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
+        | "false" -> false
+        | "true" -> true
+        | _ -> invalid_arg @@ Printf.sprintf "unkown pc option %s (expected: true, false)" pc_option in
 
         let (backend, default_dir) = match List.assoc_opt backend_str gen_backends with
             | Some x -> x
             | None -> invalid_arg @@ Printf.sprintf "unknown backend %s (supported: %s)"
                                      backend_str (String.concat ", " List.(map fst gen_backends)) in
 
-        let dir = Option.value List.(nth_opt rest 1) ~default:default_dir in
+        let dir = Option.value List.(nth_opt rest 2) ~default:default_dir in
         let cpu' = Cpu.mkCPU cpu.env cpu.denv in
-        cpu'.gen iset id backend dir;
+        cpu'.gen iset id pc_option backend dir;
         Printf.printf "Done generating %s lifter into '%s'.\n" backend_str dir;
     | ":dump" :: iset :: opcode :: rest ->
         let fname = 

dune-project

@@ -27,6 +27,7 @@
     "lwt"
     "cohttp-lwt-unix"
     "yojson"
+    "mlbdd"
   )
 )
 

libASL/asl_utils.ml

@@ -545,6 +545,35 @@ let masklength (x: string): int =
     String.iter (function ' ' -> () | _ -> r := !r + 1) x;
     !r
 
+(* Location of a statement *)
+let get_loc s =
+  match s with
+  | Stmt_If(_, _, _, _, loc)
+  | Stmt_VarDeclsNoInit(_, _, loc)
+  | Stmt_VarDecl(_, _, _, loc)
+  | Stmt_ConstDecl(_, _, _, loc)
+  | Stmt_Assign(_,_,loc)
+  | Stmt_FunReturn(_,loc)
+  | Stmt_ProcReturn(loc)
+  | Stmt_Assert(_, loc)
+  | Stmt_Unpred loc
+  | Stmt_ConstrainedUnpred loc
+  | Stmt_ImpDef (_, loc)
+  | Stmt_Undefined loc
+  | Stmt_ExceptionTaken loc
+  | Stmt_Dep_Unpred loc
+  | Stmt_Dep_Undefined loc
+  | Stmt_See (_,loc)
+  | Stmt_Throw (_, loc)
+  | Stmt_DecodeExecute (_, _, loc)
+  | Stmt_TCall (_, _, _, loc)
+  | Stmt_Case (_, _, _, loc)
+  | Stmt_For (_, _, _, _, _, loc)
+  | Stmt_While (_, _, loc)
+  | Stmt_Repeat (_, _, loc)
+  | Stmt_Try (_, _, _, _, loc)
+  | Stmt_Dep_ImpDef (_, loc) -> loc
+
 (****************************************************************)
 (** {2 Function signature accessors}                            *)
 (****************************************************************)

libASL/cpp_backend.ml

@@ -155,6 +155,7 @@ let rec prints_expr e st =
   | Expr_LitString s -> "\"" ^ s ^ "\""
   | Expr_Tuple(es) -> "std::make_tuple(" ^ (String.concat "," (List.map (fun e -> prints_expr e st) es)) ^ ")"
   | Expr_Unknown(ty) -> default_value ty st
+  | Expr_If(_, c, t, [], e) -> Printf.sprintf "((%s) ? (%s) : (%s))" (prints_expr c st) (prints_expr t st) (prints_expr e st)
 
   | _ -> failwith @@ "prints_expr: " ^ pp_expr e
 

libASL/cpu.ml

@@ -12,6 +12,7 @@ open Asl_utils
 type gen_backend =
     | Ocaml
     | Cpp
+    | Scala
 
 type gen_function = AST.ident -> Eval.fun_sig -> Eval.fun_sig Bindings.t -> Eval.fun_sig Bindings.t -> string -> unit
 
@@ -25,7 +26,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
-    gen      : string -> string -> gen_backend -> string -> unit;
+    gen      : string -> string -> bool -> gen_backend -> string -> unit;
 }
 
 let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
@@ -60,16 +61,18 @@ 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 opcode)
 
-    and gen (iset: string) (pat: string) (backend: gen_backend) (dir: string): unit =
+    and gen (iset: string) (pat: string) (include_pc: bool) (backend: gen_backend) (dir: string): unit =
         if not (Sys.file_exists dir) then failwith ("Can't find target dir " ^ dir);
 
         (* Build the symbolic lifter *)
-        let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run iset pat env in
+        let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run_marshal include_pc iset pat env in
 
         let run_gen_backend : gen_function =
             match backend with
             | Ocaml -> Ocaml_backend.run
-            | Cpp -> Cpp_backend.run in
+            | Cpp -> Cpp_backend.run
+            | Scala -> Scala_backend.run
+        in
 
         (* Build backend program *)
         run_gen_backend decoder_id decoder_fnsig tests instrs dir

libASL/cpu.mli

@@ -8,6 +8,7 @@
 type gen_backend =
     | Ocaml
     | Cpp
+    | Scala
 
 type gen_function = Asl_ast.ident -> Eval.fun_sig -> Eval.fun_sig Asl_utils.Bindings.t -> Eval.fun_sig Asl_utils.Bindings.t -> string -> unit
 
@@ -21,7 +22,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
-    gen      : string -> string -> gen_backend -> string -> unit;
+    gen      : string -> string -> bool -> gen_backend -> string -> unit;
 }
 
 val mkCPU : Eval.Env.t -> Dis.env -> cpu