Isolate Z3 into virtual library #91
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
7 tasks
katrinafyi
added a commit
that referenced
this pull request
Jun 24, 2024
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.
katrinafyi
added a commit
that referenced
this pull request
Jul 1, 2024
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.
katrinafyi
added a commit
that referenced
this pull request
Jul 1, 2024
* 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.