Merge pull request #38 from UQ-PAC/package-asl

use dune sites to install asl files

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"

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

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

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

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

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)

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

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