From d3d378bd2e7f8ad68ba499ae85483dad53cee901 Mon Sep 17 00:00:00 2001 From: rina Date: Tue, 25 Jun 2024 18:37:09 +1000 Subject: [PATCH] dummy libASL to reduce conflicts --- bin/asli.ml | 1 + bin/dune | 12 ++++++------ bin/offline_coverage.ml | 1 + bin/offline_sem.ml | 1 + bin/processops.ml | 1 + bin/server.ml | 1 + bin/testlexer.ml | 1 + libASL/dune | 16 ++++++++++------ libASL/support/dune | 2 +- libASL/support/native/dune | 3 ++- libASL/support/native/solver.ml | 3 ++- libASL/support/solver.mli | 2 +- libASL/support/web/dune | 2 +- libASL/support/web/solver.ml | 2 +- offlineASL/offline_utils.ml | 1 + tests/test_asl.ml | 1 + 16 files changed, 32 insertions(+), 18 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 50d2b6be..428483ed 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -8,6 +8,7 @@ (** ASL interactive frontend *) open LibASL +open LibASL_base open Asl_ast open Value diff --git a/bin/dune b/bin/dune index c02e79b7..7b572c03 100644 --- a/bin/dune +++ b/bin/dune @@ -5,7 +5,7 @@ (modes exe byte) (modules asli) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native linenoise pprint) + (libraries asli.libASL linenoise pprint) ) (executable @@ -14,7 +14,7 @@ (modes exe) (modules server) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native pprint 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 libASL_native offlineASL)) + (libraries asli.libASL offlineASL)) (executable (name offline_sem) @@ -47,4 +47,4 @@ (modes exe) (modules offline_sem) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native offlineASL)) + (libraries asli.libASL offlineASL)) diff --git a/bin/offline_coverage.ml b/bin/offline_coverage.ml index 6263b6f0..4d6002d8 100644 --- a/bin/offline_coverage.ml +++ b/bin/offline_coverage.ml @@ -1,4 +1,5 @@ open LibASL +open LibASL_base open Testing open Asl_ast open Value diff --git a/bin/offline_sem.ml b/bin/offline_sem.ml index 54b8ac38..63e3476f 100644 --- a/bin/offline_sem.ml +++ b/bin/offline_sem.ml @@ -1,4 +1,5 @@ open LibASL +open LibASL_base open Asl_ast open Asl_utils diff --git a/bin/processops.ml b/bin/processops.ml index cf710181..eff3dc95 100644 --- a/bin/processops.ml +++ b/bin/processops.ml @@ -1,4 +1,5 @@ open LibASL +open LibASL_base module Bindings = Asl_utils.Bindings diff --git a/bin/server.ml b/bin/server.ml index 77a14ba3..bbec4feb 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -1,4 +1,5 @@ open LibASL +open LibASL_base open Yojson diff --git a/bin/testlexer.ml b/bin/testlexer.ml index 655ced61..77f92b52 100644 --- a/bin/testlexer.ml +++ b/bin/testlexer.ml @@ -8,6 +8,7 @@ (** ASL lexer test harness *) open LibASL +open LibASL_base module Lexer = Lexer module TC = Tcheck diff --git a/libASL/dune b/libASL/dune index 1ca4d24a..e1468c6f 100644 --- a/libASL/dune +++ b/libASL/dune @@ -15,18 +15,17 @@ (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly))))) (library - (name libASL_ast) - (public_name asli.libASL-ast) + (name libASL_base) + (public_name asli.libASL-base) (flags (:standard -w -27)) - (wrapped false) (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils) (libraries pprint (re_export zarith))) (library (name libASL) - (public_name asli.libASL) + (public_name asli.libASL-virtual) (flags - (:standard -w -27 -cclib -lstdc++)) + (:standard -w -27 -cclib -lstdc++ -open LibASL_base)) (modules cpu dis elf eval lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value symbolic_lifter decoder_program call_graph req_analysis @@ -35,5 +34,10 @@ ) (preprocessor_deps (alias ../asl_files)) (preprocess (pps ppx_blob)) - (libraries libASL_support (re_export libASL_ast) str)) + (libraries libASL_support str)) +(library + (name libASL_dummy) + (public_name asli.libASL) + (modules) + (libraries (re_export libASL) libASL_native)) diff --git a/libASL/support/dune b/libASL/support/dune index 4d907e49..aed79f34 100644 --- a/libASL/support/dune +++ b/libASL/support/dune @@ -3,5 +3,5 @@ (library (name libASL_support) (public_name asli.libASL-support) - (libraries libASL_ast) + (libraries libASL_base) (virtual_modules solver)) diff --git a/libASL/support/native/dune b/libASL/support/native/dune index f01935ce..7df5046b 100644 --- a/libASL/support/native/dune +++ b/libASL/support/native/dune @@ -1,4 +1,5 @@ (library (name libASL_native) + (public_name asli.libASL-support-native) (implements libASL_support) - (libraries z3 libASL_ast)) + (libraries z3 libASL_base)) diff --git a/libASL/support/native/solver.ml b/libASL/support/native/solver.ml index 7870f10b..acac8cd9 100644 --- a/libASL/support/native/solver.ml +++ b/libASL/support/native/solver.ml @@ -17,7 +17,8 @@ we can reason that "F(x) == F(x)" without knowing "F". *) -module AST = Asl_ast +module AST = LibASL_base.Asl_ast +module Asl_utils = LibASL_base.Asl_utils let verbose = false diff --git a/libASL/support/solver.mli b/libASL/support/solver.mli index 759dcce3..764ae71a 100644 --- a/libASL/support/solver.mli +++ b/libASL/support/solver.mli @@ -3,4 +3,4 @@ (****************************************************************) (** check that bs => cs *) -val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool +val check_constraints : (LibASL_base.Asl_ast.expr list) -> (LibASL_base.Asl_ast.expr list) -> bool diff --git a/libASL/support/web/dune b/libASL/support/web/dune index 380dcf39..b69b8598 100644 --- a/libASL/support/web/dune +++ b/libASL/support/web/dune @@ -2,4 +2,4 @@ (name libASL_web) (public_name asli.libASL-web) (implements libASL_support) - (libraries libASL_ast zarith_stubs_js)) + (libraries libASL_base zarith_stubs_js)) diff --git a/libASL/support/web/solver.ml b/libASL/support/web/solver.ml index fa6b9717..111ee86e 100644 --- a/libASL/support/web/solver.ml +++ b/libASL/support/web/solver.ml @@ -1,4 +1,4 @@ -module AST = Asl_ast +module AST = LibASL_base.Asl_ast let check_constraints (_bs: AST.expr list) (_cs: AST.expr list): bool = true diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml index 6ead03b3..d33f903d 100644 --- a/offlineASL/offline_utils.ml +++ b/offlineASL/offline_utils.ml @@ -1,4 +1,5 @@ open LibASL +open LibASL_base open Asl_ast open Primops diff --git a/tests/test_asl.ml b/tests/test_asl.ml index 80c875f0..b08b45d9 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -6,6 +6,7 @@ ****************************************************************) open LibASL +open LibASL_base open Asl_utils open AST