rename libASL parts to stage0/stage1

libASL/dune

@@ -14,18 +14,27 @@
      (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_base)
- (public_name asli.libASL-base)
+ (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_virtual)
- (public_name asli.libASL-virtual)
+ (name libASL_stage1)
+ (public_name asli.libASL-stage1)
  (flags
-  (:standard -w -27 -cclib -lstdc++ -open LibASL_base))
+  (: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
@@ -34,17 +43,17 @@
    )
  (preprocessor_deps (alias ../asl_files))
  (preprocess (pps ppx_blob))
- (libraries libASL_support str))
+ (libraries libASL_stage0 libASL_support str))
 
 (library
- (name libASL)
- (public_name asli.libASL-merged)
+ (name libASL_virtual)
+ (public_name asli.libASL-virtual)
  (modules libASL)
- (wrapped false)
- (libraries libASL_virtual libASL_base))
+ (wrapped false) ; exports LibASL module
+ (libraries libASL_stage0 libASL_stage1))
 
 (library
  (name libASL_dummy)
  (public_name asli.libASL)
  (modules)
- (libraries (re_export libASL) libASL_native))
+ (libraries (re_export libASL_virtual) libASL_support_native))

libASL/libASL.ml

@@ -1,2 +1,2 @@
-include LibASL_base
-include LibASL_virtual
+include LibASL_stage0
+include LibASL_stage1

libASL/ocaml_backend.ml

@@ -382,7 +382,7 @@ let write_dune_file files dir =
     Printf.fprintf oc "    %s\n" (String.lowercase_ascii k)
   ) files;
   Printf.fprintf oc "  )
-  (libraries libASL))";
+  (libraries asli.libASL))";
   close_out oc
 
 (* Write all of the above, expecting offline_utils.ml to already be present in dir *)

libASL/support/dune

@@ -3,5 +3,5 @@
 (library
  (name libASL_support)
  (public_name asli.libASL-support)
- (libraries libASL_base)
+ (libraries libASL_stage0)
  (virtual_modules solver))

libASL/support/native/dune

@@ -1,5 +1,5 @@
 (library
- (name libASL_native)
+ (name libASL_support_native)
  (public_name asli.libASL-support-native)
  (implements libASL_support)
- (libraries z3 libASL_base))
+ (libraries z3 libASL_stage0))

libASL/support/native/solver.ml

@@ -17,8 +17,8 @@
     we can reason that "F(x) == F(x)" without knowing "F".
  *)
 
-module AST = LibASL_base.Asl_ast
-module Asl_utils = LibASL_base.Asl_utils
+module AST = LibASL_stage0.Asl_ast
+module Asl_utils = LibASL_stage0.Asl_utils
 
 let verbose = false
 

libASL/support/solver.mli

@@ -2,5 +2,7 @@
 (** {3 Z3 support code}                                         *)
 (****************************************************************)
 
+open LibASL_stage0
+
 (** check that bs => cs *)
-val check_constraints : (LibASL_base.Asl_ast.expr list) -> (LibASL_base.Asl_ast.expr list) -> bool
+val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool

libASL/support/web/dune

@@ -1,5 +1,5 @@
 (library
- (name libASL_web)
- (public_name asli.libASL-web)
+ (name libASL_support_web)
+ (public_name asli.libASL-support-web)
  (implements libASL_support)
- (libraries libASL_base zarith_stubs_js))
+ (libraries libASL_stage0 zarith_stubs_js))

libASL/support/web/solver.ml

@@ -1,4 +1,4 @@
 
-module AST = LibASL_base.Asl_ast
+module AST = LibASL_stage0.Asl_ast
 
 let check_constraints (_bs: AST.expr list) (_cs: AST.expr list): bool = true

offlineASL/dune

@@ -8,4 +8,4 @@
     decode_tests
     offline_utils
   )
-  (libraries libASL))
+  (libraries asli.libASL))

tests/dune

@@ -1,4 +1,4 @@
 (test (name test_asl)
  (modes exe)
  (flags (-cclib -lstdc++))
- (libraries alcotest libASL libASL_native))
+ (libraries alcotest asli.libASL))