diff --git a/asli.opam b/asli.opam index 2c87cf31..428c463b 100644 --- a/asli.opam +++ b/asli.opam @@ -16,7 +16,7 @@ license: "BSD-3-Clause" homepage: "https://github.com/alastairreid/asl-interpreter" bug-reports: "https://github.com/alastairreid/asl-interpreter/issues" depends: [ - "dune" {>= "2.5"} + "dune" {>= "2.8"} "ocaml" {>= "4.09"} "menhir" {build} "ott" {build & >= "0.31"} @@ -26,9 +26,11 @@ depends: [ "z3" {>= "4.8.7"} "pcre" "alcotest" {with-test} + "dune-site" + "odoc" {with-doc} ] build: [ - ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "dune" "build" diff --git a/bin/asli.ml b/bin/asli.ml index 2d2dfbe4..75bbd807 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -22,10 +22,13 @@ module AST = Asl_ast 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_verbose = ref false let opt_debug_level = ref 0 + let () = Printexc.register_printer (function | Value.EvalError (loc, msg) -> @@ -288,6 +291,8 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit = let options = Arg.align ([ ( "-x", Arg.Set_int opt_debug_level, " Debugging output"); ( "-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"); ( "--version", Arg.Set opt_print_version, " Print version"); ( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)"); ] ) @@ -312,33 +317,32 @@ let _ = (fun s -> opt_filenames := (!opt_filenames) @ [s]) usage_msg + 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 begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; - let t = LoadASL.read_file !opt_prelude true !opt_verbose in - let ts = List.map (fun filename -> - if Utils.endswith filename ".spec" then begin - LoadASL.read_spec filename !opt_verbose - end else if Utils.endswith filename ".asl" then begin - LoadASL.read_file filename false !opt_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) - end - ) !opt_filenames - in - - if !opt_verbose then Printf.printf "Building evaluation environment\n"; - let env = (try - Eval.build_evaluation_environment (List.concat (t::ts)) - with - | Value.EvalError (loc, msg) -> - Printf.printf " %s: Evaluation error: %s\n" (pp_loc loc) msg; - exit 1 - ) in + let env_opt = + if (!opt_no_default_aarch64) + then evaluation_environment !opt_prelude !opt_filenames !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 (); + end in + let env = (match env_opt with + | Some e -> e + | None -> failwith "Unable to build evaluation environment.") in + if not !opt_no_default_aarch64 then + opt_filenames := snd (Option.get aarch64_asl_files); (* (!) should be safe if environment built successfully. *) if !opt_verbose then Printf.printf "Built evaluation environment\n"; Dis.debug_level := !opt_debug_level; @@ -352,7 +356,7 @@ let main () = repl tcenv cpu end -let _ =ignore(main ()) +let _ = ignore (main ()) (**************************************************************** * End diff --git a/bin/dune b/bin/dune index 94a55ab1..26be40f7 100644 --- a/bin/dune +++ b/bin/dune @@ -1,10 +1,12 @@ + (executable (name asli) (public_name asli) (modes exe byte) (modules asli) (flags (-cclib -lstdc++)) - (libraries libASL linenoise pprint pcre)) + (libraries libASL linenoise pprint pcre) + ) (executable (name testlexer) @@ -21,3 +23,4 @@ (modules processops) (flags (-cclib -lstdc++)) (libraries libASL unix)) + diff --git a/coverage.sh b/coverage.sh index aaed68a5..923abcce 100755 --- a/coverage.sh +++ b/coverage.sh @@ -1,14 +1,12 @@ #!/bin/bash # performs regression testing based on :coverage of particular groups of instructions - -INSTRUCTION_GROUPS="aarch64_integer.+ aarch64_branch.+" +INSTRUCTION_GROUPS='' +INSTRUCTION_GROUPS+='aarch64_integer.+' +INSTRUCTION_GROUPS+=' aarch64_branch.+' INSTRUCTION_GROUPS+=' aarch64_float_.+' INSTRUCTION_GROUPS+=' aarch64_vector_.+' INSTRUCTION_GROUPS+=' aarch64_memory_.+' -ASL_FILES="prelude.asl ./mra_tools/arch/regs.asl ./mra_tools/types.asl ./mra_tools/arch/arch.asl ./mra_tools/arch/arch_instrs.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" -ASL_FILES+=" tests/override.asl" -ASL_FILES+=" tests/override.prj" COVERAGE_DIR="./tests/coverage" COVERAGE_TEMP=$(mktemp -d) @@ -26,21 +24,28 @@ fi mkdir -p "$COVERAGE_DIR" mkdir -p "$COVERAGE_TEMP" +asl_dir="$(dune exec asli -- --aarch64-dir)" + +tar xf encodings.tar.gz || exit 1 RESULT=0 for inst in $INSTRUCTION_GROUPS; do fname="$(tr -c '[:alnum:]_' _ <<< "$inst")" new="$COVERAGE_TEMP/$fname" + diff="$COVERAGE_TEMP/$fname.diff" echo "::group::$inst" echo "$new" - time echo ":coverage A64 $inst" | dune exec asli $ASL_FILES > "$new" + time echo ":coverage A64 $inst" | dune exec asli > "$new" old="$COVERAGE_DIR/$fname" + sed -i "s#$asl_dir#.#g" "$new" + if [[ $MODE == update ]]; then echo "overwriting coverage results with updated results." cp -v "$new" "$old" else echo "testing coverage with previous results." + diff -Nu "$old" "$new" > "$diff" diff -Nu --color=auto "$old" "$new" RESULT=$(($RESULT + $?)) fi diff --git a/dune b/dune new file mode 100644 index 00000000..586df531 --- /dev/null +++ b/dune @@ -0,0 +1,22 @@ +(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/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))) + ) diff --git a/dune-project b/dune-project index f1f07b1b..788c5923 100644 --- a/dune-project +++ b/dune-project @@ -1,7 +1,8 @@ -(lang dune 2.5) +(lang dune 2.8) (name asli) (version 0.2.0) +(using dune_site 0.1) (using menhir 2.0) (package @@ -24,7 +25,9 @@ ("z3" (>= "4.8.7")) "pcre" ("alcotest" :with-test) + "dune-site" ) + (sites (share aslfiles)) ) (license BSD-3-Clause) diff --git a/libASL/dune b/libASL/dune index 8197d9b6..838e32ca 100644 --- a/libASL/dune +++ b/libASL/dune @@ -19,5 +19,9 @@ (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) - (libraries pprint zarith z3 str pcre)) + lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res) + (libraries pprint zarith z3 str pcre dune-site)) + +(generate_sites_module + (module res) + (sites asli)) diff --git a/libASL/eval.ml b/libASL/eval.ml index 40403695..f46da381 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -1183,6 +1183,8 @@ and eval_encoding (env: Env.t) (x: encoding) (op: value): bool = false end + + (****************************************************************) (** {2 Creating environment from global declarations} *) (****************************************************************) @@ -1308,6 +1310,50 @@ let build_evaluation_environment (ds: AST.declaration list): Env.t = begin end + + +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 -> + if Utils.endswith filename ".spec" then begin + LoadASL.read_spec filename verbose + end else if Utils.endswith filename ".asl" then begin + LoadASL.read_file filename 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) + end + ) files + in + if verbose then Printf.printf "Building evaluation environment\n"; + (try + Some (build_evaluation_environment (List.concat (t::ts))) + with + | Value.EvalError (loc, msg) -> + Printf.printf " %s: Evaluation error: %s\n" (pp_loc loc) msg; + None + ) + +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/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)) + +(** XXX: .prj files NOT evaluated in this environment! *) +let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = + Option.bind aarch64_asl_files + (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose) + (**************************************************************** * End ****************************************************************)