Skip to content

Commit

Permalink
Merged backends (#80)
Browse files Browse the repository at this point in the history
* 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]>
  • Loading branch information
ailrst and katrinafyi authored May 22, 2024
1 parent ed09cb9 commit 4899c72
Show file tree
Hide file tree
Showing 21 changed files with 2,464 additions and 299 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -19,3 +19,6 @@ scripts/result.txt
scripts/output.txt
scripts/cntlm.bir
scripts/total.txt

.cache/
build/
5 changes: 3 additions & 2 deletions bin/asli.ml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ let opt_no_default_aarch64 = ref false
let opt_print_aarch64_dir = ref false
let opt_verbose = ref false

let opt_debug_level = ref 0
let opt_debug_level = ref (-1)


let () = Printexc.register_printer
Expand Down Expand Up @@ -60,6 +60,7 @@ let help_msg = [
let gen_backends = [
("ocaml", (Cpu.Ocaml, "offlineASL"));
("cpp", (Cpu.Cpp, "offlineASL-cpp"));
("scala", (Cpu.Scala, "offlineASL-cpp"));
]

let flags = [
Expand Down Expand Up @@ -325,7 +326,7 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit =
)

let options = Arg.align ([
( "-x", Arg.Set_int opt_debug_level, " Debugging output");
( "-x", Arg.Set_int opt_debug_level, " Partial evaluation debugging (requires debug level argument >= 0)");
( "-v", Arg.Set opt_verbose, " Verbose output");
( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics");
( "--aarch64-dir", Arg.Set opt_print_aarch64_dir, " Print directory of bundled AArch64 semantics");
Expand Down
6 changes: 3 additions & 3 deletions libASL/asl_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,7 @@ let fv_stmts stmts =

let fv_stmt stmt =
let fvs = new freevarClass in
ignore (visit_stmt (fvs :> aslVisitor) stmt);
ignore (visit_stmt_single (fvs :> aslVisitor) stmt);
fvs#result

let fv_decl decl =
Expand Down Expand Up @@ -295,7 +295,7 @@ end

let locals_of_stmts stmts =
let lc = new localsClass in
ignore (Visitor.mapNoCopy (visit_stmt (lc :> aslVisitor)) stmts);
ignore @@ Asl_visitor.visit_stmts lc stmts;
lc#locals

let locals_of_decl decl =
Expand Down Expand Up @@ -423,7 +423,7 @@ let subst_type (s: expr Bindings.t) (x: ty): ty =

let subst_stmt (s: expr Bindings.t) (x: stmt): stmt =
let subst = new substClass s in
visit_stmt subst x
visit_stmt_single subst x


(** More flexible substitution class - takes a function instead
Expand Down
648 changes: 374 additions & 274 deletions libASL/asl_visitor.ml

Large diffs are not rendered by default.

Loading

0 comments on commit 4899c72

Please sign in to comment.