From 4d0bac9814b94b916e6b8528e3e85ab1b313b015 Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Mon, 1 Jul 2024 12:09:57 +1000 Subject: [PATCH] Support compilation to Javascript (#90) * Split libASL and isolate Z3 into virtual library (#91) Z3 links to a native shared library, and so is unsuitable for use via js-of-ocaml. This separates the one use of Z3 in the code (the type-checker's constraint solver) into a separate library which may be stubbed for non-native platforms. This separates libASL into two parts: libASL_ast which is the minimum needed to define the ASL syntax tree, and libASL which contains the rest of the library. libASL should still be used as the public interface of the library. Since libASL re-exports all of libASL_ast, this should not affect the API visible by downstream users. This is required since we need to insert a platform-specific library, libASL_support, which introduces z3 only on native builds. The dependency tree now looks like: libASL_ast <- libASL_support (virtual) <- libASL. * remove pcre library, use ocaml str instead (#93) PCRE relies on a shared library, precluding its use in Javascript. instead, we use the standard ocaml "str" library. note, however, that this supports a smaller subscript of regex (notably no negative lookahead), and has a different syntax. see: https://ocaml.org/manual/5.2/api/Str.html * Embed ARM ASL specs within OCaml (#92) * extract arm environment into separate file. * allow loading files from either disk or memory * use ppx_blob to embed ASL files instead of dune-site This is instead of installing the ASL files to disk. This should make the installation less liable to random breakages when installed or linked in an unexpected way. The binary size increases by 6MB. Updates tests/coverage/run.sh to substitute away the new file paths of the embedded files, so no coverage re-generation needed. * replace --aarch64-dir with --export-aarch64 this is more useful once the MRA files are bundled. * initialising jsoo * tcheck: make global env0 mutable necessary for correct unmarshalling, as this must contain global variables * dummy libASL to reduce conflicts * rename libASL parts to stage0/stage1 --- asli.opam | 3 +- bin/asli.ml | 21 +++--- bin/dune | 12 +-- bin/offline_coverage.ml | 6 +- bin/server.ml | 2 +- dune | 44 ++++++----- dune-project | 5 +- libASL/arm_env.ml | 34 +++++++++ libASL/decoder_program.ml | 4 +- libASL/dis.ml | 6 +- libASL/dune | 49 ++++++++++--- libASL/eval.ml | 55 +++++--------- libASL/libASL.ml | 2 + libASL/loadASL.ml | 77 +++++++++++++------- libASL/loadASL.mli | 12 ++- libASL/ocaml_backend.ml | 9 ++- libASL/support/dune | 7 ++ libASL/support/native/dune | 5 ++ libASL/support/native/solver.ml | 79 ++++++++++++++++++++ libASL/support/solver.mli | 8 ++ libASL/tcheck.ml | 89 +++-------------------- libASL/testing.ml | 4 +- libASL/utils.ml | 9 +++ offlineASL/decode_tests.ml | 4 + offlineASL/dune | 11 ++- offlineASL/offline.ml | 5 +- offlineASL/{utils.ml => offline_utils.ml} | 0 tests/coverage/dune | 6 +- tests/coverage/run.sh | 4 +- tests/dune | 2 +- tests/test_asl.ml | 6 +- 31 files changed, 353 insertions(+), 227 deletions(-) create mode 100644 libASL/arm_env.ml create mode 100644 libASL/libASL.ml create mode 100644 libASL/support/dune create mode 100644 libASL/support/native/dune create mode 100644 libASL/support/native/solver.ml create mode 100644 libASL/support/solver.mli create mode 100644 offlineASL/decode_tests.ml rename offlineASL/{utils.ml => offline_utils.ml} (100%) diff --git a/asli.opam b/asli.opam index 690da900..4a09e8ae 100644 --- a/asli.opam +++ b/asli.opam @@ -24,9 +24,8 @@ depends: [ "pprint" "zarith" "z3" {>= "4.8.7"} - "pcre" "alcotest" {with-test} - "dune-site" + "ppx_blob" "lwt" "cohttp-lwt-unix" "yojson" diff --git a/bin/asli.ml b/bin/asli.ml index c00ae2bc..50d2b6be 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -23,7 +23,7 @@ let opt_prelude : string ref = ref "prelude.asl" let opt_filenames : string list ref = ref [] let opt_print_version = ref false let opt_no_default_aarch64 = ref false -let opt_print_aarch64_dir = ref false +let opt_export_aarch64_dir = ref "" let opt_verbose = ref false @@ -309,8 +309,8 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit = let options = Arg.align ([ ( "-x", Arg.Set_int Dis.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"); + ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics"); + ( "--export-aarch64", Arg.Set_string opt_export_aarch64_dir, " Export bundled AArch64 MRA to the given directory"); ( "--version", Arg.Set opt_print_version, " Print version"); ( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)"); ] ) @@ -338,25 +338,26 @@ let _ = let main () = if !opt_print_version then Printf.printf "%s\n" version - else if !opt_print_aarch64_dir then - match aarch64_asl_dir with - | Some d -> Printf.printf "%s\n" d - | None -> (Printf.eprintf "Unable to retrieve installed asl directory\n"; exit 1) + else if "" <> !opt_export_aarch64_dir then + let dir = !opt_export_aarch64_dir in + ignore @@ Sys.readdir dir; + List.iter LoadASL.(write_source dir) Arm_env.(prelude_blob :: asl_blobs); else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; + let sources = List.map (fun x -> LoadASL.FileSource x) !opt_filenames in (* Note: .prj files are handled by `evaluation_environment`. *) let env_opt = if (!opt_no_default_aarch64) - then evaluation_environment !opt_prelude !opt_filenames !opt_verbose + then evaluation_environment (FileSource !opt_prelude) sources !opt_verbose else begin if List.length (!opt_filenames) != 0 then Printf.printf "Warning: asl file arguments ignored without --no-aarch64 (%s)\n" (String.concat " " !opt_filenames) else (); - aarch64_evaluation_environment ~verbose:!opt_verbose (); + Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose (); end in let env = (match env_opt with @@ -369,7 +370,7 @@ let main () = LNoise.history_set ~max_length:100 |> ignore; let denv = Dis.build_env env in - let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in + let tcenv = TC.Env.mkEnv !TC.env0 and cpu = Cpu.mkCPU env denv in repl tcenv cpu end diff --git a/bin/dune b/bin/dune index 5927fafd..7b572c03 100644 --- a/bin/dune +++ b/bin/dune @@ -5,7 +5,7 @@ (modes exe byte) (modules asli) (flags (-cclib -lstdc++)) - (libraries libASL linenoise pprint pcre) + (libraries asli.libASL linenoise pprint) ) (executable @@ -14,7 +14,7 @@ (modes exe) (modules server) (flags (-cclib -lstdc++)) - (libraries libASL pprint pcre lwt.unix yojson cohttp-lwt cohttp-lwt-unix)) + (libraries asli.libASL pprint lwt.unix yojson cohttp-lwt cohttp-lwt-unix)) (executable @@ -23,7 +23,7 @@ ; (public_name test_asl_lexer) (modules testlexer) (flags (-cclib -lstdc++)) - (libraries libASL)) + (libraries asli.libASL)) (executable (name processops) @@ -31,7 +31,7 @@ ; (public_name test_asl_lexer) (modules processops) (flags (-cclib -lstdc++)) - (libraries libASL unix)) + (libraries asli.libASL unix)) (executable (name offline_coverage) @@ -39,7 +39,7 @@ (modes exe) (modules offline_coverage) (flags (-cclib -lstdc++)) - (libraries libASL offlineASL)) + (libraries asli.libASL offlineASL)) (executable (name offline_sem) @@ -47,4 +47,4 @@ (modes exe) (modules offline_sem) (flags (-cclib -lstdc++)) - (libraries libASL offlineASL)) + (libraries asli.libASL offlineASL)) diff --git a/bin/offline_coverage.ml b/bin/offline_coverage.ml index 147d6dc8..6263b6f0 100644 --- a/bin/offline_coverage.ml +++ b/bin/offline_coverage.ml @@ -84,13 +84,9 @@ let rec process_command tcenv env cmd = let main () = let opt_verbose = ref false in - let env = match Eval.aarch64_evaluation_environment ~verbose:!opt_verbose () with + let env = match Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose () with | Some e -> e | _ -> failwith "Unable to build evaluation environment." in - let filenames = Option.get Eval.aarch64_asl_files in - let prj_files = List.filter (fun f -> Utils.endswith f ".prj") (snd filenames) in - let tcenv = Tcheck.Env.mkEnv Tcheck.env0 in - List.iter (fun f -> process_command tcenv env (":project " ^ f)) prj_files; List.map (fun instr -> run opt_verbose instr env) !opt_instr let _ = ignore (main()) diff --git a/bin/server.ml b/bin/server.ml index fa28737d..77a14ba3 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -15,7 +15,7 @@ open Asl_utils open Lwt -let persistent_env = lazy (Option.get (aarch64_evaluation_environment ())) +let persistent_env = lazy (Option.get (Arm_env.aarch64_evaluation_environment ())) let eval_instr (opcode: string) : string = let pp_raw stmt : string = Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt) |> String.trim in diff --git a/dune b/dune index 10c8b130..6347f813 100644 --- a/dune +++ b/dune @@ -1,26 +1,24 @@ -(install - (files - (prelude.asl as prelude.asl ) - (mra_tools/arch/arch.asl as mra_tools/arch/arch.asl ) - (mra_tools/arch/arch_decode.asl as mra_tools/arch/arch_decode.asl ) - (mra_tools/arch/arch_instrs.asl as mra_tools/arch/arch_instrs.asl ) - (mra_tools/arch/regs.asl as mra_tools/arch/regs.asl ) - (mra_tools/arch/regs_access.asl as mra_tools/arch/regs_access.asl ) - (mra_tools/support/aes.asl as mra_tools/support/aes.asl ) - (mra_tools/support/barriers.asl as mra_tools/support/barriers.asl ) - (mra_tools/support/debug.asl as mra_tools/support/debug.asl ) - (mra_tools/support/feature.asl as mra_tools/support/feature.asl ) - (mra_tools/support/fetchdecode.asl as mra_tools/support/fetchdecode.asl) - (mra_tools/support/hints.asl as mra_tools/support/hints.asl ) - (mra_tools/support/interrupts.asl as mra_tools/support/interrupts.asl ) - (mra_tools/support/memory.asl as mra_tools/support/memory.asl ) - (mra_tools/support/stubs.asl as mra_tools/support/stubs.asl ) - (mra_tools/types.asl as mra_tools/types.asl ) - (tests/override.asl as tests/override.asl ) - (tests/override.prj as tests/override.prj ) - ) - (section (site (asli aslfiles))) - ) +(alias + (name asl_files) + (deps + prelude.asl + mra_tools/arch/arch.asl + mra_tools/arch/arch_decode.asl + mra_tools/arch/arch_instrs.asl + mra_tools/arch/regs.asl + mra_tools/arch/regs_access.asl + mra_tools/support/aes.asl + mra_tools/support/barriers.asl + mra_tools/support/debug.asl + mra_tools/support/feature.asl + mra_tools/support/fetchdecode.asl + mra_tools/support/hints.asl + mra_tools/support/interrupts.asl + mra_tools/support/memory.asl + mra_tools/support/stubs.asl + mra_tools/types.asl + tests/override.asl + tests/override.prj)) (alias (name default) diff --git a/dune-project b/dune-project index 6b9b8780..f57814cc 100644 --- a/dune-project +++ b/dune-project @@ -2,7 +2,6 @@ (name asli) (version 0.2.0) -(using dune_site 0.1) (using menhir 2.0) (package @@ -23,14 +22,12 @@ "pprint" "zarith" ("z3" (>= "4.8.7")) - "pcre" ("alcotest" :with-test) - "dune-site" + "ppx_blob" "lwt" "cohttp-lwt-unix" "yojson" ) - (sites (share aslfiles)) ) (license BSD-3-Clause) diff --git a/libASL/arm_env.ml b/libASL/arm_env.ml new file mode 100644 index 00000000..78557f67 --- /dev/null +++ b/libASL/arm_env.ml @@ -0,0 +1,34 @@ +(* defines the evaluation environment for the bundled Arm spsecifications. *) + +let aarch64_asl_dir: string option = + None + +let prelude_blob : LoadASL.source = DataSource ("prelude.asl", [%blob "../prelude.asl"]) + +let asl_blobs : LoadASL.source list = [ + DataSource ("mra_tools/arch/regs.asl", [%blob "../mra_tools/arch/regs.asl"]); + DataSource ("mra_tools/types.asl", [%blob "../mra_tools/types.asl"]); + DataSource ("mra_tools/arch/arch.asl", [%blob "../mra_tools/arch/arch.asl"]); + DataSource ("mra_tools/arch/arch_instrs.asl", [%blob "../mra_tools/arch/arch_instrs.asl"]); + DataSource ("mra_tools/arch/regs_access.asl", [%blob "../mra_tools/arch/regs_access.asl"]); + DataSource ("mra_tools/arch/arch_decode.asl", [%blob "../mra_tools/arch/arch_decode.asl"]); + DataSource ("mra_tools/support/aes.asl", [%blob "../mra_tools/support/aes.asl"]); + DataSource ("mra_tools/support/barriers.asl", [%blob "../mra_tools/support/barriers.asl"]); + DataSource ("mra_tools/support/debug.asl", [%blob "../mra_tools/support/debug.asl";]); + DataSource ("mra_tools/support/feature.asl", [%blob "../mra_tools/support/feature.asl"]); + DataSource ("mra_tools/support/hints.asl", [%blob "../mra_tools/support/hints.asl"]); + DataSource ("mra_tools/support/interrupts.asl", [%blob "../mra_tools/support/interrupts.asl"]); + DataSource ("mra_tools/support/memory.asl", [%blob "../mra_tools/support/memory.asl";]); + DataSource ("mra_tools/support/stubs.asl", [%blob "../mra_tools/support/stubs.asl"]); + DataSource ("mra_tools/support/fetchdecode.asl", [%blob "../mra_tools/support/fetchdecode.asl"]); + DataSource ("tests/override.asl", [%blob "../tests/override.asl"]); + DataSource ("tests/override.prj", [%blob "../tests/override.prj"]); +] + +let aarch64_asl_files: (LoadASL.source * LoadASL.source list) option = + Some (prelude_blob, asl_blobs) + +let aarch64_evaluation_environment ?(verbose = false) (): Eval.Env.t option = + Option.bind aarch64_asl_files + (fun (prelude, filenames) -> Eval.evaluation_environment prelude filenames verbose) + diff --git a/libASL/decoder_program.ml b/libASL/decoder_program.ml index 5558e71c..123352ba 100644 --- a/libASL/decoder_program.ml +++ b/libASL/decoder_program.ml @@ -116,10 +116,10 @@ let run iset pat env problematic = (* Find all matching instructions, pulled from testing.ml *) let decoder = Eval.Env.getDecoder env (Ident iset) in - let re = Pcre.regexp pat in + let re = Str.regexp pat in let filterfn = function | ((Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)),_,_,_) -> - is = iset && Pcre.pmatch ~rex:re nm && not (List.mem nm problematic) + is = iset && Str.string_match re nm 0 && not (List.mem nm problematic) | _ -> assert false in let encs = List.filter filterfn (Eval.Env.listInstructions env) in diff --git a/libASL/dis.ml b/libASL/dis.ml index b61ba338..0d2b3c22 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -180,7 +180,7 @@ module LocalEnv = struct let init (env: Eval.Env.t) = let eval e = val_expr (Eval.eval_expr Unknown env e) in - let tenv = Tcheck.env0 in + let tenv = !Tcheck.env0 in let get_global_type id = (match Tcheck.GlobalEnv.getGlobalVar tenv id with | Some (Type_Bits e) -> @@ -642,7 +642,7 @@ and width_of_type (loc: l) (t: ty): int = | _ -> unsupported loc @@ "Can't get bit width of type: " ^ pp_type t and width_of_field (loc: l) (t: ty) (f: ident): int = - let env = Tcheck.env0 in + let env = !Tcheck.env0 in let ft = (match Tcheck.typeFields env loc t with | FT_Record rfs -> Tcheck.get_recordfield loc rfs f @@ -654,7 +654,7 @@ and width_of_field (loc: l) (t: ty) (f: ident): int = (** Determine the type of memory access expression (Var, Array, Field) *) and type_of_load (loc: l) (x: expr): ty rws = - let env = Tcheck.env0 in + let env = !Tcheck.env0 in (match x with | Expr_Var(id) -> let+ (_,(t,_)) = DisEnv.gets (LocalEnv.resolveGetVar loc id) in diff --git a/libASL/dune b/libASL/dune index 6fae933e..0bb060c8 100644 --- a/libASL/dune +++ b/libASL/dune @@ -14,19 +14,46 @@ (with-stdout-to asl_parser_tail.mly (bash "OTT=${ASLI_OTT:-$(opam config var ott:share)}; grep -v '^%%' $OTT/menhir_library_extra.mly")) (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly))))) +; libASL is constructed in two stages: stage0, and stage1. +; stage0 is the minimum needed to define an "expression", and stage1 is the rest. +; this is so stage0 can be used as a dependency for the libASL_support virtual library +; which provides flexibility on whether to link z3 (for native compilation) or not (for js compilation). +; thus, everything after the type-checking phase is in stage1. +; these stages are merged together in libASL_virtual and re-exported as "LibASL", +; and asli.libASL provides a publicly available dummy library which additionally +; links the native implementation of the support code. + (library - (name libASL) - (public_name asli.libASL) + (name libASL_stage0) + (public_name asli.libASL-stage0) + (flags (:standard -w -27)) + (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils) + (libraries pprint (re_export zarith))) + +(library + (name libASL_stage1) + (public_name asli.libASL-stage1) (flags - (:standard -w -27 -cclib -lstdc++)) - (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor cpu dis elf eval - lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res + (:standard -w -27 -cclib -lstdc++ -open LibASL_stage0)) + (modules cpu dis elf eval + lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value symbolic_lifter decoder_program call_graph req_analysis - offline_transform ocaml_backend dis_tc - offline_opt + offline_transform ocaml_backend dis_tc offline_opt + arm_env ) - (libraries pprint zarith z3 str pcre dune-site)) + (preprocessor_deps (alias ../asl_files)) + (preprocess (pps ppx_blob)) + (libraries libASL_stage0 libASL_support str)) -(generate_sites_module - (module res) - (sites asli)) +(library + (name libASL_virtual) + (public_name asli.libASL-virtual) + (modules libASL) + (wrapped false) ; exports LibASL module + (libraries libASL_stage0 libASL_stage1)) + +(library + (name libASL_dummy) + (public_name asli.libASL) + (modules) + (libraries (re_export libASL_virtual) libASL_support_native)) diff --git a/libASL/eval.ml b/libASL/eval.ml index 64a25013..39859f6f 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -1319,34 +1319,37 @@ let set_impdef (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) (rest: string Env.setImpdef env x v (** Evaluates a minimal subset of the .prj syntax, sufficient for override.prj. *) -let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) = - let inchan = open_in fname in - try - while true do - let line = input_line inchan in - match (String.split_on_char ' ' line) with +let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (source: LoadASL.source) = + let data = LoadASL.read_source source in + let fname = LoadASL.pp_source source in + let lines = List.map String.trim @@ String.split_on_char '\n' data in + List.iter + (fun line -> match (String.split_on_char ' ' line) with | ":set" :: "impdef" :: rest -> set_impdef tcenv env fname rest | empty when List.for_all (String.equal "") empty -> () (* ignore empty lines *) - | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line - done - with | End_of_file -> close_in inchan + | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line) + lines (** Constructs an evaluation environment with the given prelude file and .asl/.prj files. .prj files given here are required to be minimal. *) -let evaluation_environment (prelude: string) (files: string list) (verbose: bool) = - let t = LoadASL.read_file prelude true verbose in - let ts = List.map (fun filename -> +let evaluation_environment (prelude: LoadASL.source) (files: LoadASL.source list) (verbose: bool) = + let t = LoadASL.read_file (prelude) true verbose in + let ts = List.map (fun file -> + let filename = LoadASL.name_of_source file in if Utils.endswith filename ".spec" then begin - LoadASL.read_spec filename verbose + LoadASL.read_spec file verbose end else if Utils.endswith filename ".asl" then begin - LoadASL.read_file filename false verbose + LoadASL.read_file file false verbose end else if Utils.endswith filename ".prj" then begin [] (* ignore project files here and process later *) end else begin - failwith ("Unrecognized file suffix on "^filename) + failwith ("Unrecognized file suffix on "^(LoadASL.pp_source file)) end ) files in - let prjs = List.filter (fun fname -> Utils.endswith fname ".prj") files in + + let prjs = List.filter + (fun fname -> Utils.endswith (LoadASL.name_of_source fname) ".prj") + files in if verbose then Printf.printf "Building evaluation environment\n"; let env = ( @@ -1356,29 +1359,11 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool None ) in - let tcenv = TC.Env.mkEnv Tcheck.env0 in + let tcenv = TC.Env.mkEnv !Tcheck.env0 in Option.iter (fun env -> List.iter (evaluate_prj_minimal tcenv env) prjs) env; env -let aarch64_asl_dir: string option = - List.nth_opt Res.Sites.aslfiles 0 - -let aarch64_asl_files: (string * string list) option = - let aarch64_file_load_order = - ["mra_tools/arch/regs.asl"; "mra_tools/types.asl"; "mra_tools/arch/arch.asl"; "mra_tools/arch/arch_instrs.asl"; "mra_tools/arch/regs_access.asl"; - "mra_tools/arch/arch_decode.asl"; "mra_tools/support/aes.asl"; "mra_tools/support/barriers.asl"; "mra_tools/support/debug.asl"; - "mra_tools/support/feature.asl"; "mra_tools/support/hints.asl"; "mra_tools/support/interrupts.asl"; "mra_tools/support/memory.asl"; - "mra_tools/support/stubs.asl"; "mra_tools/support/fetchdecode.asl"; "tests/override.asl"; "tests/override.prj"] - in Option.bind aarch64_asl_dir (fun dir -> - let filenames = List.map (Filename.concat dir) aarch64_file_load_order in - let prelude = Filename.concat dir "prelude.asl" in - Some (prelude, filenames)) - -let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = - Option.bind aarch64_asl_files - (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose) - (**************************************************************** * End ****************************************************************) diff --git a/libASL/libASL.ml b/libASL/libASL.ml new file mode 100644 index 00000000..8427825d --- /dev/null +++ b/libASL/libASL.ml @@ -0,0 +1,2 @@ +include LibASL_stage0 +include LibASL_stage1 diff --git a/libASL/loadASL.ml b/libASL/loadASL.ml index 3b06ed79..3c30be1a 100644 --- a/libASL/loadASL.ml +++ b/libASL/loadASL.ml @@ -23,6 +23,42 @@ let mkLoc (fname: string) (input: string): AST.l = let finish: Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = len } in AST.Range (start, finish) +(** a source of data which may be a file on disk or a byte string in memory. *) +type source = FileSource of string | DataSource of string * string + +let pp_source = function | FileSource s -> s | DataSource (name, _) -> "" + +let name_of_source = function | FileSource s | DataSource (s, _) -> s + +(** opens a variant source. + returns (lexbuf, closer) where closer should be called to close the source. *) +let open_source source = match source with + | FileSource filename -> + let inchan = open_in filename in + let lexbuf = Lexing.from_channel inchan in + lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source }; + (lexbuf, fun () -> close_in inchan) + | DataSource (filename, data) -> + let lexbuf = Lexing.from_string data in + lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source }; + (lexbuf, Fun.id) + +let read_source = function + | FileSource filename -> + let inchan = open_in_bin filename in + let x = really_input_string inchan (in_channel_length inchan) in + close_in inchan; + x + | DataSource (_, data) -> data + +let write_source prefix = function + | FileSource _ -> failwith "write_source for FileSource is unsupported" + | DataSource (name, data) -> + let name = Filename.concat prefix name in + Utils.mkdir_p (Filename.dirname name); + let chan = open_out_bin name in + output_string chan data; + close_out chan let report_parse_error (on_error: unit -> 'a) (f: unit -> 'a): 'a = (try @@ -92,10 +128,8 @@ let declare_var_getters (decls: declaration list) = in List.map declare decls -let parse_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declaration list = - let inchan = open_in filename in - let lexbuf = Lexing.from_channel inchan in - lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename }; +let parse_file (filename : source) (isPrelude: bool) (verbose: bool): AST.declaration list = + let (lexbuf, close) = open_source filename in let t = report_parse_error (fun _ -> print_endline (pp_loc (Range (lexbuf.lex_start_p, lexbuf.lex_curr_p))); exit 1) @@ -104,46 +138,39 @@ let parse_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declar let lexer = offside_token Lexer.token in (* Run the parser on this line of input. *) - if verbose then Printf.printf "- Parsing %s\n" filename; + if verbose then Printf.printf "- Parsing %s\n" (pp_source filename); Parser.declarations_start lexer lexbuf) in - close_in inchan; + close (); declare_var_getters t -let read_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declaration list = - if verbose then Printf.printf "Processing %s\n" filename; +let read_file (filename : source) (isPrelude: bool) (verbose: bool): AST.declaration list = + if verbose then Printf.printf "Processing %s\n" (pp_source filename); let t = parse_file filename isPrelude verbose in if false then PPrint.ToChannel.pretty 1.0 60 stdout (PP.pp_declarations t); - if verbose then Printf.printf " - Got %d declarations from %s\n" (List.length t) filename; + if verbose then Printf.printf " - Got %d declarations from %s\n" (List.length t) (pp_source filename); let t' = report_type_error (fun _ -> exit 1) (fun _ -> - if verbose then Printf.printf "- Typechecking %s\n" filename; + if verbose then Printf.printf "- Typechecking %s\n" (pp_source filename); TC.tc_declarations isPrelude t ) in if false then PPrint.ToChannel.pretty 1.0 60 stdout (PP.pp_declarations t'); - if verbose then Printf.printf " - Got %d typechecked declarations from %s\n" (List.length t') filename; + if verbose then Printf.printf " - Got %d typechecked declarations from %s\n" (List.length t') (pp_source filename); - if verbose then Printf.printf "Finished %s\n" filename; + if verbose then Printf.printf "Finished %s\n" (pp_source filename); flush stdout; t' -let read_spec (filename : string) (verbose: bool): AST.declaration list = - let r: AST.declaration list list ref = ref [] in - let inchan = open_in filename in - (try - while true do - let t = read_file (input_line inchan) false verbose in - r := t :: !r - done - with - | End_of_file -> - close_in inchan - ); - List.concat (List.rev !r) +let read_spec (filename : source) (verbose: bool): AST.declaration list = + let specfile = read_source filename in + let lines = String.split_on_char '\n' specfile + |> List.map String.trim + |> List.filter (fun x -> x <> "") in + List.concat_map (fun f -> read_file (FileSource f) false verbose) lines let read_impdef (tcenv: TC.Env.t) (loc: AST.l) (s: string): (string * AST.expr) = let lexbuf = Lexing.from_string s in diff --git a/libASL/loadASL.mli b/libASL/loadASL.mli index 7e1810f8..c9ef75fc 100644 --- a/libASL/loadASL.mli +++ b/libASL/loadASL.mli @@ -8,6 +8,12 @@ module AST = Asl_ast module TC = Tcheck +type source = FileSource of string | DataSource of string * string +val pp_source : source -> string +val name_of_source : source -> string +val read_source : source -> string + val write_source : string -> source -> unit + val mkLoc : string -> string -> AST.l val report_parse_error : (unit -> 'a) -> (unit -> 'a) -> 'a @@ -15,12 +21,12 @@ val report_type_error : (unit -> 'a) -> (unit -> 'a) -> 'a val report_eval_error : (unit -> 'a) -> (unit -> 'a) -> 'a (** Parse and typecheck ASL file *) -val read_file : string -> bool -> bool -> Asl_ast.declaration list +val read_file : source -> bool -> bool -> Asl_ast.declaration list -val read_spec : string -> bool -> Asl_ast.declaration list +val read_spec : source -> bool -> Asl_ast.declaration list (** Parse ASL file, but do not typecheck *) -val parse_file : string -> bool -> bool -> Asl_ast.declaration list +val parse_file : source -> bool -> bool -> Asl_ast.declaration list val read_impdef : TC.Env.t -> AST.l -> string -> (string * AST.expr) val read_expr : TC.Env.t -> AST.l -> string -> AST.expr diff --git a/libASL/ocaml_backend.ml b/libASL/ocaml_backend.ml index d6e421e2..7c1f725c 100644 --- a/libASL/ocaml_backend.ml +++ b/libASL/ocaml_backend.ml @@ -333,7 +333,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 = ["Utils"] +let global_deps = ["Offline_utils"] (* Write an instruction file, containing just the behaviour of one instructions *) let write_instr_file fn fnsig dir = @@ -372,7 +372,8 @@ let write_decoder_file fn fnsig deps dir = (* Write the dune build file *) let write_dune_file files dir = let oc = open_out (dir ^ "/dune") in - Printf.fprintf oc "(library + Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND +(library (name offlineASL) (flags (:standard -w -27 -w -33 -cclib -lstdc++)) @@ -381,10 +382,10 @@ let write_dune_file files dir = Printf.fprintf oc " %s\n" (String.lowercase_ascii k) ) files; Printf.fprintf oc " ) - (libraries zarith libASL))"; + (libraries asli.libASL))"; close_out oc -(* Write all of the above, expecting Utils.ml to already be present in dir *) +(* Write all of the above, expecting offline_utils.ml to already be present in dir *) let run dfn dfnsig tests fns dir = 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 diff --git a/libASL/support/dune b/libASL/support/dune new file mode 100644 index 00000000..fc6ca707 --- /dev/null +++ b/libASL/support/dune @@ -0,0 +1,7 @@ +; provides platform-specific dependencies + +(library + (name libASL_support) + (public_name asli.libASL-support) + (libraries libASL_stage0) + (virtual_modules solver)) diff --git a/libASL/support/native/dune b/libASL/support/native/dune new file mode 100644 index 00000000..3281f961 --- /dev/null +++ b/libASL/support/native/dune @@ -0,0 +1,5 @@ +(library + (name libASL_support_native) + (public_name asli.libASL-support-native) + (implements libASL_support) + (libraries z3 libASL_stage0)) diff --git a/libASL/support/native/solver.ml b/libASL/support/native/solver.ml new file mode 100644 index 00000000..5611d7a3 --- /dev/null +++ b/libASL/support/native/solver.ml @@ -0,0 +1,79 @@ +(****************************************************************) +(** {3 Z3 support code} *) +(****************************************************************) + +(** Convert ASL expression to Z3 expression. + This only copes with a limited set of operations: ==, +, -, * and DIV. + (It is possible that we will need to extend this list in the future but + it is sufficient for the current ASL specifications.) + + The support for DIV is not sound - it is a hack needed to cope with + the way ASL code is written and generally needs a side condition + that the division is exact (no remainder). + + ufs is a mutable list of conversions used to handle subexpressions + that cannot be translated. We treat such subexpressions as + uninterpreted functions and add them to the 'ufs' list so that + we can reason that "F(x) == F(x)" without knowing "F". + *) + +module AST = LibASL_stage0.Asl_ast +module Asl_utils = LibASL_stage0.Asl_utils + +let verbose = false + +let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr = + (match x with + | Expr_Var(v) -> + let intsort = Z3.Arithmetic.Integer.mk_sort ctx in + Z3.Expr.mk_const_s ctx (AST.pprint_ident v) intsort + | Expr_Parens y -> z3_of_expr ctx ufs y + | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i + + (* todo: the following lines involving DIV are not sound *) + | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a + | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b + | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]); + Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])]) + when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2" + -> z3_of_expr ctx ufs a1 + | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) -> + Z3.Boolean.mk_eq ctx + (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a]) + (z3_of_expr ctx ufs b) + + | Expr_TApply (FIdent ("add_int",_), [], xs) -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs) + | Expr_TApply (FIdent ("sub_int",_), [], xs) -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs) + | Expr_TApply (FIdent ("mul_int",_), [], xs) -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs) + | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b) + | Expr_TApply (FIdent ("eq_int",_), [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b) + | _ -> + if verbose then Printf.printf " Unable to translate %s - using as uninterpreted function\n" (Asl_utils.pp_expr x); + let intsort = Z3.Arithmetic.Integer.mk_sort ctx in + (match List.assoc_opt x !ufs with + | None -> + let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in + ufs := (x, uf) :: !ufs; + uf + | Some uf -> + uf + ) + ) + +(** check that bs => cs *) +let check_constraints (bs: AST.expr list) (cs: AST.expr list): bool = + (* note that we rebuild the Z3 context each time. + * It is possible to share them across all invocations to save + * about 10% of execution time. + *) + let z3_ctx = Z3.mk_context [] in + let solver = Z3.Solver.mk_simple_solver z3_ctx in + let ufs = ref [] in (* uninterpreted function list *) + let bs' = List.map (z3_of_expr z3_ctx ufs) bs in + let cs' = List.map (z3_of_expr z3_ctx ufs) cs in + let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in + if verbose then Printf.printf " - Checking %s\n" (Z3.Expr.to_string p); + Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p]; + let q = Z3.Solver.check solver [] in + if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p); + q = UNSATISFIABLE diff --git a/libASL/support/solver.mli b/libASL/support/solver.mli new file mode 100644 index 00000000..88c3ed21 --- /dev/null +++ b/libASL/support/solver.mli @@ -0,0 +1,8 @@ +(****************************************************************) +(** {3 Z3 support code} *) +(****************************************************************) + +open LibASL_stage0 + +(** check that bs => cs *) +val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool diff --git a/libASL/tcheck.ml b/libASL/tcheck.ml index 7a53c82a..b4086797 100644 --- a/libASL/tcheck.ml +++ b/libASL/tcheck.ml @@ -709,83 +709,14 @@ let rec simplify_expr (x: AST.expr): AST.expr = (** Perform simple constant folding of expressions within a type *) let simplify_type (x: AST.ty): AST.ty = let repl = new replaceExprClass (fun e -> Some (simplify_expr e)) in - Asl_visitor.visit_type repl x - + Visitor.visit_type repl x (****************************************************************) -(** {3 Z3 support code} *) +(** {3 Constraint solver entry point} *) (****************************************************************) -(** Convert ASL expression to Z3 expression. - This only copes with a limited set of operations: ==, +, -, * and DIV. - (It is possible that we will need to extend this list in the future but - it is sufficient for the current ASL specifications.) - - The support for DIV is not sound - it is a hack needed to cope with - the way ASL code is written and generally needs a side condition - that the division is exact (no remainder). - - ufs is a mutable list of conversions used to handle subexpressions - that cannot be translated. We treat such subexpressions as - uninterpreted functions and add them to the 'ufs' list so that - we can reason that "F(x) == F(x)" without knowing "F". - *) - -let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr = - (match x with - | Expr_Var(v) -> - let intsort = Z3.Arithmetic.Integer.mk_sort ctx in - Z3.Expr.mk_const_s ctx (pprint_ident v) intsort - | Expr_Parens y -> z3_of_expr ctx ufs y - | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i - - (* todo: the following lines involving DIV are not sound *) - | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a - | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b - | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]); - Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])]) - when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2" - -> z3_of_expr ctx ufs a1 - | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) -> - Z3.Boolean.mk_eq ctx - (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a]) - (z3_of_expr ctx ufs b) - - | Expr_TApply (FIdent ("add_int",_), [], xs) -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs) - | Expr_TApply (FIdent ("sub_int",_), [], xs) -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs) - | Expr_TApply (FIdent ("mul_int",_), [], xs) -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs) - | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b) - | Expr_TApply (FIdent ("eq_int",_), [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b) - | _ -> - if verbose then Printf.printf " Unable to translate %s - using as uninterpreted function\n" (pp_expr x); - let intsort = Z3.Arithmetic.Integer.mk_sort ctx in - (match List.assoc_opt x !ufs with - | None -> - let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in - ufs := (x, uf) :: !ufs; - uf - | Some uf -> - uf - ) - ) - -(** check that bs => cs *) let check_constraints (bs: expr list) (cs: expr list): bool = - (* note that we rebuild the Z3 context each time. - * It is possible to share them across all invocations to save - * about 10% of execution time. - *) - let z3_ctx = Z3.mk_context [] in - let solver = Z3.Solver.mk_simple_solver z3_ctx in - let ufs = ref [] in (* uninterpreted function list *) - let bs' = List.map (z3_of_expr z3_ctx ufs) bs in - let cs' = List.map (z3_of_expr z3_ctx ufs) cs in - let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in - if verbose then Printf.printf " - Checking %s\n" (Z3.Expr.to_string p); - Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p]; - let q = Z3.Solver.check solver [] in - if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p); - q = UNSATISFIABLE + LibASL_support.Solver.check_constraints bs cs (****************************************************************) @@ -897,7 +828,7 @@ class unifier (loc: AST.l) (assumptions: expr list) = object (self) (* attempt to close an expression by replacing all fresh vars with a closed expression *) and close_expr (x: expr): expr option = let subst = new substFunClass (fun x -> if self#isFresh x then Some (close_ident x) else None) in - let x' = Asl_visitor.visit_expr subst x in + let x' = Visitor.visit_expr subst x in if isClosed x' then Some x' else @@ -1027,8 +958,8 @@ let unify_ixtype (u: unifier) (ty1: AST.ixtype) (ty2: AST.ixtype): unit = let rec unify_type (env: GlobalEnv.t) (u: unifier) (ty1: AST.ty) (ty2: AST.ty): unit = (* Substitute global constants in types *) let subst_consts = new substFunClass (GlobalEnv.getConstant env) in - let ty1' = Asl_visitor.visit_type subst_consts ty1 in - let ty2' = Asl_visitor.visit_type subst_consts ty2 in + let ty1' = Visitor.visit_type subst_consts ty1 in + let ty2' = Visitor.visit_type subst_consts ty2 in (match (derefType env ty1', derefType env ty2') with | (Type_Constructor c1, Type_Constructor c2) -> () | (Type_Bits(e1), Type_Bits(e2)) -> u#addEquality e1 e2 @@ -2517,11 +2448,11 @@ let genPrototypes (ds: AST.declaration list): (AST.declaration list * AST.declar (List.rev !pre, List.rev !post) (** Overall typechecking environment shared by all invocations of typechecker *) -let env0 = GlobalEnv.mkempty () +let env0 = ref (GlobalEnv.mkempty ()) (** Typecheck a list of declarations - main entrypoint into typechecker *) let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaration list = - if verbose then Printf.printf " - Using Z3 %s\n" Z3.Version.to_string; + (* if verbose then Printf.printf " - Using Z3 %s\n" Z3.Version.to_string; *) (* Process declarations, starting by moving all function definitions to the * end of the list and replacing them with function prototypes. * As long as the type/var decls are all sorted correctly, this @@ -2532,8 +2463,8 @@ let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaratio *) let (pre, post) = if isPrelude then (ds, []) else genPrototypes ds in if verbose then Printf.printf " - Typechecking %d phase 1 declarations\n" (List.length pre); - let pre' = List.map (tc_declaration env0) pre in - let post' = List.map (tc_declaration env0) post in + let pre' = List.map (tc_declaration !env0) pre in + let post' = List.map (tc_declaration !env0) post in if verbose then List.iter (fun ds -> List.iter (fun d -> Printf.printf "\nTypechecked %s\n" (Utils.to_string (PP.pp_declaration d))) ds) post'; if verbose then Printf.printf " - Typechecking %d phase 2 declarations\n" (List.length post); List.append (List.concat pre') (List.concat post') diff --git a/libASL/testing.ml b/libASL/testing.ml index c1f58f06..be51e87e 100644 --- a/libASL/testing.ml +++ b/libASL/testing.ml @@ -423,10 +423,10 @@ let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult = let get_opcodes (opt_verbose: bool ref) (iset: string) (instr: string) (env: Env.t): (string * instr_field list * ((int * bool) list) option) list = if !opt_verbose then Printf.printf "Coverage for encoding %s\n" instr; - let re = Pcre.regexp instr in + let re = Str.regexp instr in let encoding_matches = function | (Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)) -> - is = iset && Pcre.pmatch ~rex:re nm + is = iset && Str.string_match re nm 0 | _ -> assert false in let encs = List.map (fun (x,_,_,_) -> x) (Env.listInstructions env) in diff --git a/libASL/utils.ml b/libASL/utils.ml index e71887df..cc0917c1 100644 --- a/libASL/utils.ml +++ b/libASL/utils.ml @@ -7,6 +7,15 @@ (** Generic utility functions *) +let rec mkdir_p p = + let open Filename in + if Sys.file_exists p then + () + else + (* make parents, then make final directory. *) + (mkdir_p (dirname p); Sys.mkdir p 0o755) + + (**************************************************************** * Pretty-printer related ****************************************************************) diff --git a/offlineASL/decode_tests.ml b/offlineASL/decode_tests.ml new file mode 100644 index 00000000..3f44e593 --- /dev/null +++ b/offlineASL/decode_tests.ml @@ -0,0 +1,4 @@ +(* AUTO-GENERATED LIFTER FILE *) + +open Offline_utils + diff --git a/offlineASL/dune b/offlineASL/dune index b2231230..aa2cf6f6 100644 --- a/offlineASL/dune +++ b/offlineASL/dune @@ -1,6 +1,11 @@ +; AUTO-GENERATED BY OCAML BACKEND (library (name offlineASL) (flags - (:standard -w -27 -cclib -lstdc++)) - (modules offline utils) - (libraries zarith libASL)) + (:standard -w -27 -w -33 -cclib -lstdc++)) + (modules + offline + decode_tests + offline_utils + ) + (libraries asli.libASL)) diff --git a/offlineASL/offline.ml b/offlineASL/offline.ml index 719ef1f7..1d913f9b 100644 --- a/offlineASL/offline.ml +++ b/offlineASL/offline.ml @@ -1,4 +1,7 @@ -open Utils +(* AUTO-GENERATED LIFTER FILE *) + +open Offline_utils +open Decode_tests let f_A64_decoder v_enc : unit = failwith "unsupported" diff --git a/offlineASL/utils.ml b/offlineASL/offline_utils.ml similarity index 100% rename from offlineASL/utils.ml rename to offlineASL/offline_utils.ml diff --git a/tests/coverage/dune b/tests/coverage/dune index 718b8ba1..9de2105d 100644 --- a/tests/coverage/dune +++ b/tests/coverage/dune @@ -20,8 +20,10 @@ (rule (with-stdout-to cov_branch (run ./run "aarch64_branch.+"))) (rule (with-stdout-to cov_float (run ./run "aarch64_float_.+"))) (rule (with-stdout-to cov_vector1 (run ./run "aarch64_vector_arithmetic_binary.+"))) -(rule (with-stdout-to cov_vector2 (run ./run "aarch64_vector_(?!arithmetic_binary).+"))) +(rule (with-stdout-to cov_vector2 (run ./run "aarch64_vector_\\(arithmetic_unary\\|[^a]\\).+"))) (rule (with-stdout-to cov_memory (run ./run "aarch64_memory_.+"))) +; note: cov_vector2 is intended to be every vector instruction that's not arithmetic_binary. +; note ocaml Str regex syntax: https://ocaml.org/manual/5.2/api/Str.html (rule (alias coverage) (action (diff ./aarch64_integer cov_integer))) (rule (alias coverage) (action (diff ./aarch64_branch cov_branch))) @@ -34,7 +36,7 @@ (rule (with-stdout-to off_cov_branch (run ./off_run "aarch64_branch.+"))) (rule (with-stdout-to off_cov_float (run ./off_run "aarch64_float_.+"))) (rule (with-stdout-to off_cov_vector1 (run ./off_run "aarch64_vector_arithmetic_binary.+"))) -(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_(?!arithmetic_binary).+"))) +(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_\\(arithmetic_unary\\|[^a]\\).+"))) (rule (with-stdout-to off_cov_memory (run ./off_run "aarch64_memory_.+"))) (rule (alias offline-coverage) (action (diff ./aarch64_integer off_cov_integer))) diff --git a/tests/coverage/run.sh b/tests/coverage/run.sh index 0b9eebac..375dfdd4 100755 --- a/tests/coverage/run.sh +++ b/tests/coverage/run.sh @@ -2,7 +2,7 @@ pattern="${1:?requires regex pattern as first argument}" -asl_dir="$(asli --aarch64-dir)" output="$(echo ":coverage A64 $pattern" | asli)" -echo "$output" | sed "s#$asl_dir#.#g" +# substitute paths of the form with ./[...] +echo "$output" | sed 's#]*\)>#./\1#g' diff --git a/tests/dune b/tests/dune index 1c01889f..0c1c3027 100644 --- a/tests/dune +++ b/tests/dune @@ -1,4 +1,4 @@ (test (name test_asl) (modes exe) (flags (-cclib -lstdc++)) - (libraries alcotest libASL)) + (libraries alcotest asli.libASL)) diff --git a/tests/test_asl.ml b/tests/test_asl.ml index cb35f83b..80c875f0 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -12,7 +12,7 @@ open AST module TC = Tcheck module AST = Asl_ast -let mra_tools () = [ +let mra_tools () = List.map (fun x -> LoadASL.FileSource x) [ "../../../mra_tools/arch/regs.asl"; "../../../mra_tools/types.asl"; "../../../mra_tools/arch/arch.asl"; @@ -99,9 +99,9 @@ let test_compare env () : unit = ) let tests : unit Alcotest.test_case list = - let prelude = LoadASL.read_file "../../../prelude.asl" true false in + let prelude = LoadASL.read_file (FileSource "../../../prelude.asl") true false in let mra = List.map (fun tool -> LoadASL.read_file tool false false) (mra_tools ()) in - let tcenv = TC.Env.mkEnv TC.env0 in + let tcenv = TC.Env.mkEnv !TC.env0 in let env = Eval.build_evaluation_environment (prelude @ List.concat mra) in [ ("arith", `Quick, test_arith tcenv env);