From 1279becbbb52400652f83adc9f3acb2f4acba071 Mon Sep 17 00:00:00 2001 From: Albin Coquereau <6535385+ACoquereau@users.noreply.github.com> Date: Tue, 23 Mar 2021 12:03:45 +0100 Subject: [PATCH] Js worker (#456) * Add feature to parse a string as an input file * Add a webworker for Alt-Ergo * Add a small web example that uses the alt-ergo webworker * Add documentation for the worker and its example * Fix formatter * Add the webworker build in javascript workflow in the ci --- .github/workflows/build_js.yml | 36 +- .github/workflows/build_make.yml | 4 + .gitignore | 7 +- Makefile | 27 +- docs/sphinx_docs/Install/index.md | 30 +- docs/sphinx_docs/Usage/index.md | 54 +- dune-project | 1 + rsc/extra/subgraphs.dot | 22 +- rsc/extra/worker_example.html | 17 + rsc/extra/worker_json_example.json | 55 ++ src/bin/common/input_frontend.ml | 4 + src/bin/js/dune | 29 + src/bin/js/index.mld | 49 +- src/bin/js/options_interface.ml | 186 +++++ src/bin/js/options_interface.mli | 18 + src/bin/js/worker_example.ml | 254 +++++++ src/bin/js/worker_interface.ml | 982 +++++++++++++++++++++++++++ src/bin/js/worker_interface.mli | 229 +++++++ src/bin/js/worker_js.ml | 256 +++++++ src/lib/frontend/frontend.ml | 12 +- src/lib/frontend/input.ml | 2 + src/lib/frontend/input.mli | 3 + src/lib/reasoners/sat_solver_sig.mli | 4 + src/lib/structures/explanation.ml | 23 +- src/lib/structures/explanation.mli | 5 +- src/lib/util/options.ml | 29 +- src/parsers/parsers.ml | 9 + src/parsers/parsers.mli | 7 + 28 files changed, 2307 insertions(+), 47 deletions(-) create mode 100644 rsc/extra/worker_example.html create mode 100644 rsc/extra/worker_json_example.json create mode 100644 src/bin/js/options_interface.ml create mode 100644 src/bin/js/options_interface.mli create mode 100644 src/bin/js/worker_example.ml create mode 100644 src/bin/js/worker_interface.ml create mode 100644 src/bin/js/worker_interface.mli create mode 100644 src/bin/js/worker_js.ml diff --git a/.github/workflows/build_js.yml b/.github/workflows/build_js.yml index 253505ab6..1b55ccafe 100644 --- a/.github/workflows/build_js.yml +++ b/.github/workflows/build_js.yml @@ -1,12 +1,8 @@ name: Build Javascript -# this worflow try to build and test the javascript version of Alt-Ergo -# It only runs on `next` or `main` branch -on: - push: - branches: - - next - - main +# this worflow try to build and test the nodejs compatible version of Alt-Ergo +# and try to build the webworker of Alt-Ergo +on: [push,pull_request] env: OCAML_DEFAULT_VERSION: 4.10.0 @@ -21,7 +17,6 @@ env: jobs: compile_and_test_js: # check if the project build in js. - # If this test fails, no tests are done name: Compile AE with JsoO and test it with NodeJs runs-on: ubuntu-latest @@ -63,7 +58,7 @@ jobs: - name: Install deps run: opam install ./*.opam --deps-only --with-test - # Add alt-ergo-js dependencies + # Add alt-ergo.js dependencies - name: Install Js_of_ocaml and zarith_stubs_js run: opam install js_of_ocaml zarith_stubs_js @@ -73,7 +68,7 @@ jobs: run: opam install zarith.1.11 # compile Alt-Ergo with Js_of_ocaml - - name: Make alt-ergo-js + - name: Make alt-ergo.js run: opam exec -- make js-node # Use Node Js actions @@ -85,11 +80,30 @@ jobs: - name: Run simple example with node run: opam exec -- node alt-ergo.js non-regression/valid/everything/f1.ae - # Upload Alt-Ergo.js an artifact + # Upload Alt-Ergo.js as an artifact # the artifact name contains the system is builded on and the ocaml # compiler version used - name: Upload alt-ergo.js uses: actions/upload-artifact@v2 + if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/next' with: name: alt-ergo-js-${{ runner.os }}-${{ env.OCAML_DEFAULT_VERSION }} path: "alt-ergo.js" + + # Add alt-ergo-worker.js dependencies + - name: Install data-encoding js_of_ocaml-lwt + run: opam install data-encoding js_of_ocaml-lwt + + # compile the Alt-Ergo web worker with Js_of_ocaml + - name: Make alt-ergo-worker.js + run: opam exec -- make js-worker + + # Upload Alt-Ergo-worker.js as an artifact + # the artifact name contains the system is builded on and the ocaml + # compiler version used + - name: Upload alt-ergo-worker.js + uses: actions/upload-artifact@v2 + if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/next' + with: + name: alt-ergo-worker-js-${{ runner.os }}-${{ env.OCAML_DEFAULT_VERSION }} + path: "alt-ergo-worker.js" diff --git a/.github/workflows/build_make.yml b/.github/workflows/build_make.yml index f3a300d51..7cd03ae55 100644 --- a/.github/workflows/build_make.yml +++ b/.github/workflows/build_make.yml @@ -132,6 +132,10 @@ jobs: - name: Make ${{ matrix.package }} run: opam exec -- make ${{ matrix.package }} + # Clean repo + - name: Unpin the repo + run: opam pin remove . + make_install: # Test every install/uninstall rules name: Make install diff --git a/.gitignore b/.gitignore index 8610650ac..f2b1fe2c4 100644 --- a/.gitignore +++ b/.gitignore @@ -35,4 +35,9 @@ mlw tmp/ *.tmp alt-ergo/tmp/ -_opam \ No newline at end of file +_opam + +# Generated javascript files +alt-ergo.js +alt-ergo-worker.js +www/ diff --git a/Makefile b/Makefile index 97c78076f..ad425a607 100644 --- a/Makefile +++ b/Makefile @@ -51,7 +51,7 @@ SPHINXBUILD = sphinx-build # - .ml files generated by menhir or ocamllex # (since they reside in dune specific directory) GENERATED_USEFUL=$(UTIL_DIR)/config.ml $(BTEXT_DIR)/flags.dune -GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs +GENERATED_LINKS=alt-ergo altgr-ergo alt-ergo.js alt-ergo-worker.js AB-Why3-plugin.cma AB-Why3-plugin.cmxs fm-simplex-plugin.cma fm-simplex-plugin.cmxs GENERATED=$(GENERATED_USEFUL) $(GENERATED_LINKS) @@ -316,7 +316,24 @@ js-node: gen $(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/main_text_js.bc.js ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/main_text_js.bc.js alt-ergo.js -.PHONY: js-node +# Build a web worker for alt-ergo +# zarith_stubs_js, data-encoding, js_of_ocaml and js_of_ocaml-lwt packages are needed for this rule +js-worker: gen + $(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_js.bc.js + ln -sf $(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \ + +# Build a small web example using the alt-ergo web worker +# This example is available in the www/ directory +# zarith_stubs_js, data-encoding, js_of_ocaml and js_of_ocaml-lwt js_of_ocaml-ppx lwt_ppx packages are needed for this rule +js-example: js-worker + $(DUNE) build $(DUNE_FLAGS) --profile=release $(BJS_DIR)/worker_example.bc.js + mkdir -p www + cp $(EXTRA_DIR)/worker_example.html www/index.html + cd www \ + && ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_js.bc.js alt-ergo-worker.js \ + && ln -sf ../$(DEFAULT_DIR)/$(BJS_DIR)/worker_example.bc.js alt-ergo-main.js + +.PHONY: js-node js-worker js-example # ================ # Dependency graph @@ -393,6 +410,10 @@ generated-clean: dune-clean: $(DUNE) clean +# Clean js example files +js-clean: + rm -rf www + # Clean ocamldot's build artifacts ocamldot-clean: cd $(EXTRA_DIR)/ocamldot && $(MAKE) clean @@ -405,7 +426,7 @@ makefile-distclean: generated-clean release-distclean: rm -rf public-release -.PHONY: generated-clean dune-clean makefile-distclean release-distclean +.PHONY: generated-clean dune-clean js-clean makefile-distclean release-distclean emacs-edit: emacs `find . -name '*'.ml* | grep -v _build | grep -v _opam` & diff --git a/docs/sphinx_docs/Install/index.md b/docs/sphinx_docs/Install/index.md index 8ebf78b2d..1dad925a5 100644 --- a/docs/sphinx_docs/Install/index.md +++ b/docs/sphinx_docs/Install/index.md @@ -101,7 +101,7 @@ depending on whether ocamlopt is installed or only ocamlc is detected. 2. Install with `make install-gui` -#### Alt-Ergo in javascript +#### Alt-Ergo with Nodejs 1. Compile with `make js-node` @@ -111,6 +111,34 @@ Js_of_ocaml-compiler zarith_stubs_js ``` +#### Alt-Ergo web worker + + 1. Compile with `make js-worker` + +For this build rule you will need the following aditional libraries : +``` +js_of_ocaml +js_of_ocaml-lwt +zarith_stubs_js +data-encoding +``` + +#### Alt-Ergo web worker small example + + 1. Compile with `make js-example` + +This command create a `www/` directory in which you can find a small js example running in the `index.html` file + +For this build rule you will need the following aditional libraries : +``` +js_of_ocaml +js_of_ocaml-lwt +js_of_ocaml-ppx +lwt_ppx +zarith_stubs_js +data-encoding +``` + ### Plugins The steps below will build and install additional plugins (extension diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 4f8e6ee51..4c37ea4e7 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -83,9 +83,11 @@ On windows, a binary at path `Z:\some\path\bin\alt-ergo` will look for preludes plugins in `Z:\some\path\share\alt-ergo\preludes` and `Z:\some\path\share\alt-ergo\plugins` respectively. -### Javascript +## Javascript -Alt-Ergo can be compiled in Javascript see [INSTALL.md] for more informations. +Alt-Ergo can be compiled in Javascript see the [install section] for more informations. + +### Js-node The Javascript version of Alt-Ergo compatible with node-js is executed with the following command: @@ -93,6 +95,54 @@ The Javascript version of Alt-Ergo compatible with node-js is executed with the Note that timeout options and zip files are not supported with this version because of the lack of js primitives. +### Js-worker + +A web worker of the alt-ergo solver is available with the command `make js-worker`. It uses Js_of_ocaml Worker's and Lwt. The `data-encoding` library is used to encode and decode messages to/from the worker. Since the messages are in JSon format, the Alt-Ergo worker can be used from any javascript code. + +#### Inputs + +This web worker takes a json file composed of a list of string representing each line of an input file. This json file can also be composed of an optional worker identifier (integer) and an optional name for the file to solve. The following code shows an example of a such json file : + +``` +{"filename": "testfile", + "worker_id": 42, + "content": [ "goal g : true" ] } +``` + +The worker also take a Json file that correspond to the options to set in Alt-Ergo, like the following example : + +``` +{"debug": true, + "sat_solver": "Tableaux", + "steps_bound": 1000 } +``` + +#### Outpus + +At the end of solving it returns a Json file corresponding to results, debug informations, etc: + +``` +{"worker_id": 42, "status": { "Unsat": 0 }, +"results": [ "Valid (0.1940) (0 steps) (goal g)", "" ], +"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver", "" ], +"model": [ "[all-models] No SAT models found", "" ], +"unsat_core": [ "unsat-core:", "", "", "" ], +"errors": [ "" ], +"warnings": [ "" ], +"statistics": [ [], [] ] } +``` + +Options and results formats are available in `worker_interface` module. In this module you can also find functions to easily encode inputs and decode outputs. +Look at the `worker_json_example.json` in the ressources `rsc` of the project to learn more. + +### Js-worker example + +A small example of how to use the Alt-Ergo web worker can be build with the command ```make js-example```. This command also makes the web worker if it has not already been built. It produces a `www` directory with an html page where you can write a small example, run the worker, and see the results. You can also look at the console of your browser to look at the json file sent + + +[install section]: ../Install/index.md +[Lwt]: https://ocsigen.org/lwt/ +[js_of_ocaml]: https://ocsigen.org/js_of_ocaml/ [API documentation]: ../API/index.md [AB-Why3 README]: ../Plugins/ab_why3.md [Input section]: ../Input_file_formats/index diff --git a/dune-project b/dune-project index 510d55832..917facb93 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,5 @@ (lang dune 2.0) +(allow_approximate_merlin) ; Since we want to generate opam files we need to provide informations ; (generate_opam_files true) diff --git a/rsc/extra/subgraphs.dot b/rsc/extra/subgraphs.dot index 35be67b45..0bb60c717 100644 --- a/rsc/extra/subgraphs.dot +++ b/rsc/extra/subgraphs.dot @@ -34,24 +34,42 @@ subgraph cluster_bin { label="BIN"; style=filled; color=lightgray; + subgraph cluster_bin__common { + label="Common"; + style=filled; + color=lightblue; + "Input_frontend"; + "Parse_command"; + "Signals_profiling"; + "Solving_loop"; + } subgraph cluster_bin__text { label="Text"; style=filled; color=lightblue; - "Main_input"; "Main_text"; - "Main_gui"; } subgraph cluster_bin__gui { label="Gui"; style=filled; color=lightblue; + "Main_gui" "Gui_replay"; "Gui_session"; "Gui_config"; "Annoted_ast"; "Connected_ast"; } + subgraph cluster_bin__js { + label="JS"; + style=filled; + color=lightblue; + "Main_text_js"; + "Options_interface"; + "Worker_example"; + "Worker_interface"; + "Worker_js"; + } } subgraph cluster_plugins { diff --git a/rsc/extra/worker_example.html b/rsc/extra/worker_example.html new file mode 100644 index 000000000..458cc6062 --- /dev/null +++ b/rsc/extra/worker_example.html @@ -0,0 +1,17 @@ + + + + + + Alt-Ergo JS + + + + + + + + +
+ + diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json new file mode 100644 index 000000000..df4ee9502 --- /dev/null +++ b/rsc/extra/worker_json_example.json @@ -0,0 +1,55 @@ +// Example of json file that contains a filename and the content of the file +{ "filename": "Try-alt-ergo", + "worker_id": 42, + "content": + "type 'a set\n\nlogic empty : 'a set\nlogic add : 'a , 'a set -> 'a set\n\\logic mem : 'a , 'a set -> prop\n\naxiom mem_empty:\n forall x : 'a.\n not mem(x, empty : 'a set)\n\naxiom mem_add:\n forall x, y : 'a. forall s : 'a set.\n mem(x, add(y, s)) <->\n (x = y or mem(x, s))\n\nlogic is1, is2 : int set\nlogic iss : int set set\n\ngoal g_4:\n is1 = is2 -> \n (not mem(1, add(2+3, empty : int set))) and\n mem (is1, add (is2, iss)) " +} + +// Example of Json file that represent all options that can be set in the worker : +{ + "debug": false, "debug_ac": false, "debug_adt": false, + "debug_arith": false, "debug_arrays": false, "debug_bitv": false, + "debug_cc": false, "debug_combine": false, "debug_constr": false, + "debug_explanations": false, "debug_fm": false, "debug_fpa": 0, + "debug_gc": false, "debug_interpretation": false, "debug_ite": false, + "debug_matching": 0, "debug_sat": false, "debug_split": false, + "debug_sum": false, "debug_triggers": false, "debug_types": false, + "debug_typing": false, "debug_uf": false, "debug_unsat_core": false, + "debug_use": false, "debug_warnings": false, "rule": 0, + "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false, + "max_split": 0, "replay": false, "replay_all_used_context": false, + "save_used_context": false, "answers_with_loc": false, + "answers_with_loc": false, "frontend": "Legacy", "input_format": "Native", + "infer_input_format": false, "parse_only": false, "parsers": [], + "preludes": [], "type_only": false, "type_smt2": false, + "disable_weaks": false, "enable_assertions": false, "age_bound": 100, + "fm_cross_limit": 100, "steps_bound": 1000, "interpretation": 3, + "model": "MAll", "output_format": "Smtlib2", "infer_output_format": false, + "unsat_core": false, "verbose": false, "greedy": false, + "instanciate_after_backjump": false, "max_multi_triggers_size": 4, + "nb_triggers": 2, "no_ematching": false, "no_user_triggers": false, + "normalize_instances": false, "triggers_var": false, + "arith_matchin": false, "bottom_classes": false, + "cdcl_tableaux_inst": false, "cdcl_tableaux_th": false, + "disable_flat_formulas_simplifiaction": false, "enable_restarts": false, + "minimal_bj": false, "no_backjumping": false, "no_backward": false, + "no_decisions": false, "no_decisions_on": [], "no_sat_learning": false, + "sat_solver": "Tableaux", "tableaux_cdcl": false, "disable_ites": false, + "inline_lets": false, "rewriting": false, "term_like_pp": false, + "disable_adts": false, "no_ac": false, "no_contracongru": false, + "no_fm": false, "no_nla": false, "no_tcp": false, "no_theory": false, + "restricted": false, "tighten_vars": false, "use_fpa": false, + "timers": false, "file": "try-alt-ergo" +} + +// Example of Json file that represent the results from a run of the Worker +{ + "worker_id": 42, "status": { "Unsat": 0 }, + "results": [ "Valid (0.1940) (0 steps) (goal g)", "" ], + "debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver", "" ], + "model": [ "[all-models] No SAT models found", "" ], + "unsat_core": [ "unsat-core:", "", "", "" ] + "errors": [ "" ], + "warnings": [ "" ], + "statistics": [ [], [] ], +} diff --git a/src/bin/common/input_frontend.ml b/src/bin/common/input_frontend.ml index b3c2541d4..60c835fed 100644 --- a/src/bin/common/input_frontend.ml +++ b/src/bin/common/input_frontend.ml @@ -21,6 +21,10 @@ let register_legacy () = type parsed = Parsed.decl + let parse_file ~content ~format = + let l = Parsers.parse_problem_as_string ~content ~format in + Lists.to_seq l + let parse_files ~filename ~preludes = let l = Parsers.parse_problem ~filename ~preludes in Lists.to_seq l diff --git a/src/bin/js/dune b/src/bin/js/dune index 10a50f8cc..8a9c2dc2d 100644 --- a/src/bin/js/dune +++ b/src/bin/js/dune @@ -8,3 +8,32 @@ (flags --no-source-map) ) ) + +(library + (name worker_interface) + (libraries js_of_ocaml data-encoding) + (modules worker_interface) +) + +; Rule to build a web worker running Alt-Ergo +(executable + (name worker_js) + (libraries worker_interface alt_ergo_common zarith_stubs_js js_of_ocaml js_of_ocaml-lwt) + (modules worker_js options_interface) + (modes byte js) + (js_of_ocaml + (flags --no-source-map) + ) +) + +; Rule to build a small js example running the Alt-Ergo web worker +(executable + (name worker_example) + (libraries worker_interface zarith_stubs_js js_of_ocaml js_of_ocaml-lwt) + (modules worker_example) + (modes byte js) + (preprocess (pps js_of_ocaml-ppx lwt_ppx)) + (js_of_ocaml + (flags --no-source-map) + ) +) diff --git a/src/bin/js/index.mld b/src/bin/js/index.mld index a76a79773..7ed5d881b 100644 --- a/src/bin/js/index.mld +++ b/src/bin/js/index.mld @@ -5,8 +5,55 @@ A simple javascript version of the alt-ergo package is available with the command [make js-node]. The command [make js-node] will create the javascript file [alt-ergo.js]. This file allows you to run alt-ergo in command line with [node] like [node alt-ergo.js ]. -This command uses the Alt-Ergo_common internal lib (see {{:index_common.html}[Alt_ergo_common]}) for parsing command line, input file, and main solving loop. +This command uses the Alt-Ergo_common internal lib (see {{:../alt-ergo/index_common.html}[Alt_ergo_common]}) for parsing command line, input file, and main solving loop. To run this command you will need the following aditionnal dependencies: [js_of_ocaml-compiler] and [zarith_stubs_js]. The [--timeout] option is ignored due to a lack of js primitives Zip files are not recognised file extension. + +{2 The Alt-ergo web worker} + +A web worker of the alt-ergo solver is available with the command [make js-worker]. It uses Js_of_ocaml Worker's and Lwt. The [data-encoding] library is used to encode and decode messages to/from the worker. + +{3 Inputs } + +This web worker takes a json file composed of a list of string representing each line of an input file. This json file can also be composed of an optional worker identifier (integer) and an optional name for the file to solve. The following code shows an example of a such json file : + +[ {"filename": "testfile", "worker_id": 42, "content": [ "goal g : true" ] } ] + +The worker also take a Json file that correspond to the options to set in Alt-Ergo, like the following example : + +[ {"debug": true, "sat_solver": "Tableaux", "steps_bound": 1000} ] + +{3 Outpus } + +At the end of solving it returns a Json file corresponding to results, debug informations, etc: + +[ { "worker_id": 42, "status": { "Unsat": 0 }, +"results": [ "Valid (0.1940) (0 steps) (goal g)", "" ], +"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver", "" ], +"model": [ "[all-models] No SAT models found", "" ], +"unsat_core": [ "unsat-core:", "", "", "" ], +"errors": [ "" ], +"warnings": [ "" ], +"statistics": [ [], [] ], + } ] + +Options and results formats are available in {!module:Worker_interface.worker_interface} module. +Look at the [worker_json_example.json] in the ressources [rsc] of the project to learn more. + +{3 Dependancies} + +To run [make js-worker] you will need the following additionnal dependencies: [js_of_ocaml] [js_of_ocaml-lwt] [data-encoding] and [zarith_stubs_js]. + +The [--timeout] option is ignored due to a lack of js primitives +Zip files are not recognised file extension. + +{2 The Alt-ergo web worker small example} + +A small example of how to use the Alt-Ergo web worker can be build with the command [make js-example]. This command also makes the web worker if it has not already been built. It produces a [www] directory with an [index.html] file. + +To run this command you will need the following aditionnal dependencies: [js_of_ocaml] [js_of_ocaml-lwt] [js_of_ocaml-ppx] [data-encoding] and [lwt_ppx]. + +The [--timeout] option is ignored due to a lack of js primitives but a timeout can be set using lwt sleep function. +Zip files are not recognised file extension. diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml new file mode 100644 index 000000000..24181df41 --- /dev/null +++ b/src/bin/js/options_interface.ml @@ -0,0 +1,186 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +open AltErgoLib +open Worker_interface + +let get_case_split_policy = function + | None -> None + | Some csp -> match csp with + | AfterTheoryAssume -> Some Util.AfterTheoryAssume + | BeforeMatching -> Some Util.BeforeMatching + | AfterMatching -> Some Util.AfterMatching + +let get_input_format = function + | None -> None + | Some f -> match f with + | Native -> Some Options.Native + | Smtlib2 -> Some Options.Smtlib2 + | Why3 -> Some Options.Why3 + | Unknown s -> Some (Options.Unknown s) + +let get_output_format = function + | None -> None + | Some f -> match f with + | Native -> Some Options.Native + | Smtlib2 -> Some Options.Smtlib2 + | Why3 -> Some Options.Why3 + | Unknown s -> Some (Options.Unknown s) + +let get_sat_solver = function + | None -> None + | Some s -> match s with + | CDCL -> Some Util.CDCL + | CDCL_Tableaux -> Some Util.CDCL_Tableaux + | Tableaux -> Some Util.Tableaux + | Tableaux_CDCL -> Some Util.Tableaux_CDCL + +let get_instantiation_heuristic = function + | None -> None + | Some m -> match m with + | INormal -> Some Options.INormal + | IAuto -> Some Options.IAuto + | IGreedy -> Some Options.IGreedy + +let get_no_decisions_on = function + | None -> None + | Some l -> + Some (List.fold_left (fun acc d -> + Util.SS.add d acc + ) Util.SS.empty l) + +let get_frontend = function + None -> None + | Some f -> match f with + | Legacy -> Some "legacy" + | Unknown f -> Some f + +let get_numbers = function + None -> None + | Some i -> Some (Numbers.Q.from_int i) + +let set_options_opt f = function + | None -> () + | Some v -> f v + +let set_options r = + set_options_opt Options.set_frontend (get_frontend r.frontend); + set_options_opt Options.set_debug r.debug; + set_options_opt Options.set_debug_ac r.debug_ac ; + set_options_opt Options.set_debug_adt r.debug_adt ; + set_options_opt Options.set_debug_arith r.debug_arith; + set_options_opt Options.set_debug_arrays r.debug_arrays; + set_options_opt Options.set_debug_bitv r.debug_bitv; + set_options_opt Options.set_debug_cc r.debug_cc; + set_options_opt Options.set_debug_combine r.debug_combine; + set_options_opt Options.set_debug_constr r.debug_constr; + set_options_opt Options.set_debug_explanations r.debug_explanations; + set_options_opt Options.set_debug_fm r.debug_fm; + set_options_opt Options.set_debug_fpa r.debug_fpa; + set_options_opt Options.set_debug_gc r.debug_gc; + set_options_opt Options.set_debug_interpretation r.debug_interpretation; + set_options_opt Options.set_debug_ite r.debug_ite; + set_options_opt Options.set_debug_matching r.debug_matching; + set_options_opt Options.set_debug_sat r.debug_sat; + set_options_opt Options.set_debug_split r.debug_split; + set_options_opt Options.set_debug_sum r.debug_sum; + set_options_opt Options.set_debug_triggers r.debug_triggers; + set_options_opt Options.set_debug_types r.debug_types; + set_options_opt Options.set_debug_typing r.debug_typing; + set_options_opt Options.set_debug_uf r.debug_uf; + set_options_opt Options.set_debug_unsat_core r.debug_unsat_core; + set_options_opt Options.set_debug_use r.debug_use; + set_options_opt Options.set_debug_warnings r.debug_warnings; + set_options_opt Options.set_rule r.rule; + + set_options_opt Options.set_case_split_policy + (get_case_split_policy r.case_split_policy); + set_options_opt Options.set_enable_adts_cs r.enable_adts_cs; + set_options_opt Options.set_max_split (get_numbers r.max_split); + + set_options_opt Options.set_replay r.replay; + set_options_opt Options.set_replay_all_used_context + r.replay_all_used_context; + set_options_opt Options.set_replay_used_context r.replay_used_context; + set_options_opt Options.set_save_used_context r.save_used_context; + + set_options_opt Options.set_answers_with_loc r.answers_with_loc; + set_options_opt Options.set_input_format + (get_input_format r.input_format); + Options.set_infer_input_format (get_input_format r.input_format); + set_options_opt Options.set_parse_only r.parse_only; + set_options_opt Options.set_parsers r.parsers; + set_options_opt Options.set_preludes r.preludes; + set_options_opt Options.set_type_only r.type_only; + set_options_opt Options.set_type_smt2 r.type_smt2; + + set_options_opt Options.set_disable_weaks r.disable_weaks; + set_options_opt Options.set_enable_assertions r.enable_assertions; + + set_options_opt Options.set_age_bound r.age_bound; + set_options_opt Options.set_fm_cross_limit (get_numbers r.fm_cross_limit); + set_options_opt Options.set_steps_bound r.steps_bound; + + set_options_opt Options.set_interpretation r.interpretation; + + set_options_opt Options.set_output_format + (get_output_format r.output_format); + Options.set_infer_output_format (get_input_format r.output_format); + set_options_opt Options.set_unsat_core r.unsat_core; + + set_options_opt Options.set_verbose r.verbose; + + set_options_opt Options.set_instantiation_heuristic + (get_instantiation_heuristic r.instantiation_heuristic); + set_options_opt Options.set_instantiate_after_backjump + r.instantiate_after_backjump; + set_options_opt Options.set_max_multi_triggers_size r.max_multi_triggers_size; + set_options_opt Options.set_nb_triggers r.nb_triggers; + set_options_opt Options.set_no_ematching r.no_ematching; + set_options_opt Options.set_no_user_triggers r.no_user_triggers; + set_options_opt Options.set_normalize_instances r.normalize_instances; + set_options_opt Options.set_triggers_var r.triggers_var; + + set_options_opt Options.set_arith_matching r.arith_matching; + set_options_opt Options.set_bottom_classes r.bottom_classes; + set_options_opt Options.set_cdcl_tableaux_inst r.cdcl_tableaux_inst; + set_options_opt Options.set_cdcl_tableaux_th r.cdcl_tableaux_th; + set_options_opt Options.set_disable_flat_formulas_simplification + r.disable_flat_formulas_simplification; + set_options_opt Options.set_enable_restarts r.enable_restarts; + set_options_opt Options.set_minimal_bj r.minimal_bj; + set_options_opt Options.set_no_backjumping r.no_backjumping; + set_options_opt Options.set_no_backward r.no_backward; + set_options_opt Options.set_no_decisions r.no_decisions; + set_options_opt Options.set_no_decisions_on + (get_no_decisions_on r.no_decisions_on); + set_options_opt Options.set_no_sat_learning r.no_sat_learning; + set_options_opt Options.set_sat_solver (get_sat_solver r.sat_solver); + set_options_opt Options.set_tableaux_cdcl r.tableaux_cdcl; + + set_options_opt Options.set_disable_ites r.disable_ites; + set_options_opt Options.set_inline_lets r.inline_lets; + set_options_opt Options.set_rewriting r.rewriting; + set_options_opt Options.set_term_like_pp r.term_like_pp; + + set_options_opt Options.set_disable_adts r.disable_adts; + set_options_opt Options.set_no_ac r.no_ac; + set_options_opt Options.set_no_contracongru r.no_contracongru; + set_options_opt Options.set_no_fm r.no_fm; + set_options_opt Options.set_no_nla r.no_nla; + set_options_opt Options.set_no_tcp r.no_tcp; + set_options_opt Options.set_no_theory r.no_theory; + set_options_opt Options.set_restricted r.restricted; + set_options_opt Options.set_tighten_vars r.tighten_vars; + set_options_opt Options.set_use_fpa r.use_fpa; + set_options_opt Options.set_timers r.timers; + + set_options_opt Options.set_file r.file; diff --git a/src/bin/js/options_interface.mli b/src/bin/js/options_interface.mli new file mode 100644 index 000000000..b0da59ee7 --- /dev/null +++ b/src/bin/js/options_interface.mli @@ -0,0 +1,18 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +(** {1 Options interface module} *) + +(** This module aims to set options of the Alt-Ergo's lib that are set in + the worker_interface options type *) + +(** Function use to set Alt-Ergo's options from worker_interface options type *) +val set_options : Worker_interface.options -> unit diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml new file mode 100644 index 000000000..8ddb90093 --- /dev/null +++ b/src/bin/js/worker_example.ml @@ -0,0 +1,254 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +open Js_of_ocaml +open Js_of_ocaml_lwt + +module Html = Dom_html + +let document = Html.window##.document + +(* Example of the file to prove *) +let file = ref "goal g : true" + +(* This is the extension needed for the parser and corresponding to the input + file format*) +let extension = ref ".ae" + +(* Timeout *) +let timeout = ref 100. + +(* Function that run the worker. *) +let exec worker file options = + (* create a cancelable promise that can be cancel in case of timeout *) + let t, resolver = Lwt.task () in + (* Set the behaviour of the worker when Lwt send an on_cancel input *) + Lwt.on_cancel t (fun () -> worker##terminate); + (* Get the messages returned from the worker and return them *) + worker##.onmessage := + (Js_of_ocaml.Dom_html.handler (fun msg -> + let res = msg##.data in + Lwt.wakeup resolver res; + Js_of_ocaml.Js._true)); + (* Start the worker with the correspondin input, here file_options *) + worker##postMessage (file,options); + t + +(* Create the web worker and launch 2 threads. + The first one for the timeout, + the second on for the call to Alt-Ergo through his web worker *) +let solve () = + let options = + {(Worker_interface.init_options ()) with + input_format=Some Native; + file = Some "try-alt-ergo"; + debug = Some true; + verbose = Some true; + answers_with_loc = Some false; + interpretation = Some 1; + sat_solver = Some Worker_interface.Tableaux; + unsat_core = Some true; + } in + + let worker = Worker.create "./alt-ergo-worker.js" in + + (Lwt.pick [ + (let%lwt () = Lwt_js.sleep !timeout in + Lwt.return {(Worker_interface.init_results ()) with + debugs =Some ["Timeout"]}); + ( + let file = String.split_on_char '\n' !file in + let json_file = Worker_interface.file_to_json None (Some 42) file in + Firebug.console##log json_file; + let json_options = Worker_interface.options_to_json options in + Firebug.console##log json_options; + let%lwt results = exec worker json_file json_options in + Firebug.console##log results; + let res = Worker_interface.results_from_json results in + Lwt.return res + ) + ] + ) + +let string_input f area_name area = + let res = document##createDocumentFragment in + Dom.appendChild res (document##createTextNode (Js.string area_name)); + Dom.appendChild res (Html.createBr document); + let input = f document in + input##.value := Js.string !area; + input##.onchange := + Html.handler (fun _ -> + (try area := Js.to_string input##.value + with Invalid_argument _ -> ()); + input##.value := Js.string !area; + Js._false); + Dom.appendChild res input; + Dom.appendChild res (Html.createBr document); + res + +let float_input name value = + let res = document##createDocumentFragment in + Dom.appendChild res (document##createTextNode (Js.string name)); + Dom.appendChild res (Html.createBr document); + let input = Html.createInput document in + input##.value := Js.string (string_of_float !value); + input##.onchange := + Html.handler (fun _ -> + (try value := float_of_string (Js.to_string input##.value) + with Invalid_argument _ -> ()); + input##.value := Js.string (string_of_float !value); + Js._false); + Dom.appendChild res input; + Dom.appendChild res (Html.createBr document); + res + +let button name callback = + let res = document##createDocumentFragment in + let input = Html.createInput ~_type:(Js.string "submit") document in + input##.value := Js.string name; + input##.onclick := Html.handler callback; + Dom.appendChild res input; + res + +let process_results = function + | Some r -> + Some (String.concat "" r) + | None -> None + +let result = document##createTextNode (Js.string "") +(* update result text area *) +let print_res = function + | Some res -> + result##.data := Js.string res + | None -> () + +let error = document##createTextNode (Js.string "") +(* update error text area *) +let print_error = function + | Some err -> + error##.data := Js.string err + | None -> () + +let warning = document##createTextNode (Js.string "") +(* update warning text area *) +let print_warning = function + | Some wrn -> + warning##.data := Js.string wrn + | None -> () + +let debug = document##createTextNode (Js.string "") +(* update error text area *) +let print_debug = function + | Some dbg -> + debug##.data := Js.string dbg + | None -> () + +let model = document##createTextNode (Js.string "") +(* update model text area *) +let print_model = function + | Some mdl -> + model##.data := Js.string mdl + | None -> () + +let unsat_core = document##createTextNode (Js.string "") +(* update unsat core text area *) +let print_unsat_core = function + | Some usc -> unsat_core##.data := Js.string usc + | None -> () + +let statistics = document##createTextNode (Js.string "") +(* update statistics text area *) +let print_statistics = function + | None -> () + | Some l -> + let stats = List.fold_left (fun acc (name,begin_pos,end_pos,nb,used) -> + let used = match used with + | Worker_interface.Used -> "Used" + | Worker_interface.Unused -> "Unused" + | Worker_interface.Unknown -> "_" + in + (Format.sprintf "%s \n %s (%d-%d) #%d: %s" + acc name begin_pos end_pos nb used) + ) "" l in + statistics##.data := Js.string stats + +let onload _ = + let main = Js.Opt.get (document##getElementById (Js.string "main")) + (fun () -> assert false) in + (* Create a text area for the input file *) + Dom.appendChild main + (string_input Html.createTextarea "Input file to solve" file); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the extension format *) + Dom.appendChild main (string_input Html.createInput "Extension" extension); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the timeout value *) + Dom.appendChild main (float_input "Timeout" timeout); + Dom.appendChild main (Html.createBr document); + (* Create a button to start the solving *) + Dom.appendChild + main + (button "Ask Alt-Ergo" (fun _ -> + let div = Html.createDiv document in + Dom.appendChild main div; + Lwt_js_events.async (fun () -> + (* Print "solving" until the end of the solving + or until the timeout *) + print_res (Some "Solving"); + print_error (Some ""); + let%lwt res = solve () in + (* Update results area *) + print_res (process_results res.results); + (* Update errors area if errors occurs at solving *) + print_error (process_results res.errors); + (* Update warning area if warning occurs at solving *) + print_warning (process_results res.warnings); + (* Update debug area *) + print_debug (process_results res.debugs); + (* Update model *) + print_model (process_results res.model); + (* Update unsat core *) + print_unsat_core (process_results res.unsat_core); + (* Update statistics *) + print_statistics res.statistics; + Lwt.return_unit); + Js._false)); + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the results *) + Dom.appendChild main result; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the errors *) + Dom.appendChild main error; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the warning *) + Dom.appendChild main warning; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the debug *) + Dom.appendChild main debug; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the model *) + Dom.appendChild main model; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the unsat_core *) + Dom.appendChild main unsat_core; + Dom.appendChild main (Html.createBr document); + Dom.appendChild main (Html.createBr document); + (* Create a text area for the statistics *) + Dom.appendChild main statistics; + Js._false + +let _ = Html.window##.onload := Html.handler onload diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml new file mode 100644 index 000000000..b7a77c703 --- /dev/null +++ b/src/bin/js/worker_interface.ml @@ -0,0 +1,982 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present please contact us to clarify licensing. *) +(* *) +(******************************************************************************) +open Js_of_ocaml +open Data_encoding + +(** Types extract from AltErgoLib Utils.util and Utils.options *) + +type input_format = Native | Smtlib2 | Why3 (* | SZS *) | Unknown of string +type output_format = input_format + +let format_encoding = + union [ + case(Tag 1) + ~title:"Native" + (constant "Native") + (function Native -> Some () | _ -> None) + (fun () -> Native); + case(Tag 2) + ~title:"Smtlib2" + (constant "Smtlib2") + (function Smtlib2 -> Some () | _ -> None) + (fun () -> Smtlib2); + case(Tag 3) + ~title:"Why3" + (constant "Why3") + (function Why3 -> Some () | _ -> None) + (fun () -> Why3); + case(Tag 4) + ~title:"Unknown" + (obj1 (req "Unknown" string)) + (function Unknown s -> Some s | _ -> None) + (fun s -> Unknown(s)); + ] + +type case_split_policy = + | AfterTheoryAssume (* default *) + | BeforeMatching + | AfterMatching + +let case_split_policy_encoding = + union [ + case(Tag 1) + ~title:"AfterTheoryAssume" + (constant "AfterTheoryAssume") + (function AfterTheoryAssume -> Some () | _ -> None) + (fun () -> AfterTheoryAssume); + case(Tag 2) + ~title:"BeforeMatching" + (constant "BeforeMatching") + (function BeforeMatching -> Some () | _ -> None) + (fun () -> BeforeMatching); + case(Tag 3) + ~title:"AfterMatching" + (constant "AfterMatching") + (function AfterMatching -> Some () | _ -> None) + (fun () -> AfterMatching); + ] + +type sat_solver = + | Tableaux + | Tableaux_CDCL + | CDCL + | CDCL_Tableaux + +let sat_solver_encoding = + union [ + case(Tag 1) + ~title:"Tableaux" + (constant "Tableaux") + (function Tableaux -> Some () | _ -> None) + (fun () -> Tableaux); + case(Tag 2) + ~title:"Tableaux_CDCL" + (constant "Tableaux_CDCL") + (function Tableaux_CDCL -> Some () | _ -> None) + (fun () -> Tableaux_CDCL); + case(Tag 3) + ~title:"CDCL" + (constant "CDCL") + (function CDCL -> Some () | _ -> None) + (fun () -> CDCL); + case(Tag 4) + ~title:"CDCL_Tableaux" + (constant "CDCL_Tableaux") + (function CDCL_Tableaux -> Some () | _ -> None) + (fun () -> CDCL_Tableaux); + ] + +type frontend = + | Legacy + | Unknown of string + +let frontend_encoding = + union [ + case(Tag 1) + ~title:"Legacy" + (constant "Legacy") + (function Legacy -> Some () | _ -> None) + (fun () -> Legacy); + case(Tag 2) + ~title:"Unknown" + (obj1 (req "Unknown" string)) + (function Unknown s -> Some s | _ -> None) + (fun s -> Unknown(s)); + ] + +type instantiation_heuristic = INormal | IAuto | IGreedy + +let instantiation_heuristic_encoding = + union [ + case(Tag 1) + ~title:"INormal" + (constant "INormal") + (function INormal -> Some () | _ -> None) + (fun () -> INormal); + case(Tag 2) + ~title:"IAuto" + (constant "IAuto") + (function IAuto -> Some () | _ -> None) + (fun () -> IAuto); + case(Tag 3) + ~title:"IGreedy" + (constant "IGreedy") + (function IGreedy -> Some () | _ -> None) + (fun () -> IGreedy); + ] + +type options = { + debug : bool option; + debug_ac : bool option; + debug_adt : bool option; + debug_arith : bool option; + debug_arrays : bool option; + debug_bitv : bool option; + debug_cc : bool option; + debug_combine : bool option; + debug_constr : bool option; + debug_explanations : bool option; + debug_fm : bool option; + debug_fpa : int option; + debug_gc : bool option; + debug_interpretation : bool option; + debug_ite : bool option; + debug_matching : int option; + debug_sat : bool option; + debug_split : bool option; + debug_sum : bool option; + debug_triggers : bool option; + debug_types : bool option; + debug_typing : bool option; + debug_uf : bool option; + debug_unsat_core : bool option; + debug_use : bool option; + debug_warnings : bool option; + rule : int option; + + case_split_policy : case_split_policy option; + enable_adts_cs : bool option; + max_split : int option; + + replay : bool option; + replay_all_used_context : bool option; + replay_used_context : bool option; + save_used_context : bool option; + + answers_with_loc : bool option; + frontend : frontend option; + input_format : input_format option; + parse_only : bool option; + parsers : (string list) option; + preludes : (string list) option; + type_only : bool option; + type_smt2 : bool option; + + disable_weaks : bool option; + enable_assertions : bool option; + + age_bound : int option; + fm_cross_limit : int option; + steps_bound : int option; + + interpretation : int option; + + output_format : output_format option; + unsat_core : bool option; + + + verbose : bool option; + + instantiation_heuristic : instantiation_heuristic option; + instantiate_after_backjump : bool option; + max_multi_triggers_size : int option; + nb_triggers : int option; + no_ematching : bool option; + no_user_triggers : bool option; + normalize_instances : bool option; + triggers_var : bool option; + + arith_matching : bool option; + bottom_classes : bool option; + cdcl_tableaux_inst : bool option; + cdcl_tableaux_th : bool option; + disable_flat_formulas_simplification : bool option; + enable_restarts : bool option; + minimal_bj : bool option; + no_backjumping : bool option; + no_backward : bool option; + no_decisions : bool option; + no_decisions_on : (string list) option; + no_sat_learning : bool option; + sat_solver : sat_solver option; + tableaux_cdcl : bool option; + + disable_ites : bool option; + inline_lets : bool option; + rewriting : bool option; + term_like_pp : bool option; + + disable_adts : bool option; + no_ac : bool option; + no_contracongru : bool option; + no_fm : bool option; + no_nla : bool option; + no_tcp : bool option; + no_theory : bool option; + restricted : bool option; + tighten_vars : bool option; + use_fpa : bool option; + timers : bool option; + + file : string option; +} + +let init_options () = { + debug = None; + debug_ac = None; + debug_adt = None; + debug_arith = None; + debug_arrays = None; + debug_bitv = None; + debug_cc = None; + debug_combine = None; + debug_constr = None; + debug_explanations = None; + debug_fm = None; + debug_fpa = None; + debug_gc = None; + debug_interpretation = None; + debug_ite = None; + debug_matching = None; + debug_sat = None; + debug_split = None; + debug_sum = None; + debug_triggers = None; + debug_types = None; + debug_typing = None; + debug_uf = None; + debug_unsat_core = None; + debug_use = None; + debug_warnings = None; + rule = None; + + case_split_policy = None; + enable_adts_cs = None; + max_split = None; + + replay = None; + replay_all_used_context = None; + replay_used_context = None; + save_used_context = None; + + answers_with_loc = None; + frontend = None; + input_format = None; + parse_only = None; + parsers = None; + preludes = None; + type_only = None; + type_smt2 = None; + + disable_weaks = None; + enable_assertions = None; + + age_bound = None; + fm_cross_limit = None; + steps_bound = None; + + interpretation = None; + + output_format = None; + unsat_core = None; + + + verbose = None; + + instantiation_heuristic = None; + instantiate_after_backjump = None; + max_multi_triggers_size = None; + nb_triggers = None; + no_ematching = None; + no_user_triggers = None; + normalize_instances = None; + triggers_var = None; + + arith_matching = None; + bottom_classes = None; + cdcl_tableaux_inst = None; + cdcl_tableaux_th = None; + disable_flat_formulas_simplification = None; + enable_restarts = None; + minimal_bj = None; + no_backjumping = None; + no_backward = None; + no_decisions = None; + no_decisions_on = None; + no_sat_learning = None; + sat_solver = None; + tableaux_cdcl = None; + + disable_ites = None; + inline_lets = None; + rewriting = None; + term_like_pp = None; + + disable_adts = None; + no_ac = None; + no_contracongru = None; + no_fm = None; + no_nla = None; + no_tcp = None; + no_theory = None; + restricted = None; + tighten_vars = None; + use_fpa = None; + timers = None; + + file = None; +} + + +let opt_dbg1_encoding = + conv + (fun dbg1 -> dbg1) + (fun dbg1 -> dbg1) + (obj10 + (opt "debug" bool) + (opt "debug_ac" bool) + (opt "debug_adt" bool) + (opt "debug_arith" bool) + (opt "debug_arrays" bool) + (opt "debug_bitv" bool) + (opt "debug_cc" bool) + (opt "debug_combine" bool) + (opt "debug_constr" bool) + (opt "debug_explanations" bool) + ) + +let opt_dbg2_encoding = + conv + (fun dbg2 -> dbg2) + (fun dbg2 -> dbg2) + (obj10 + (opt "debug_fm" bool) + (opt "debug_fpa" int31) + (opt "debug_gc" bool) + (opt "debug_interpretation" bool) + (opt "debug_ite" bool) + (opt "debug_matching" int31) + (opt "debug_sat" bool) + (opt "debug_split" bool) + (opt "debug_sum" bool) + (opt "debug_triggers" bool) + ) + +let opt_dbg3_encoding = + conv + (fun dbg3 -> dbg3) + (fun dbg3 -> dbg3) + (obj6 + (opt "debug_types" bool) + (opt "debug_typing" bool) + (opt "debug_uf" bool) + (opt "debug_unsat_core" bool) + (opt "debug_use" bool) + (opt "debug_warnings" bool) + ) + +let opt1_encoding = + conv + (fun opt1 -> opt1) + (fun opt1 -> opt1) + (obj8 + (opt "rule" int31) + (opt "case_split_policy" case_split_policy_encoding) + (opt "enable_adts_cs" bool) + (opt "max_split" int31) + (opt "replay" bool) + (opt "replay_all_used_context" bool) + (opt "save_used_context" bool) + (opt "answers_with_loc" bool) + ) + +let opt2_encoding = + conv + (fun opt2 -> opt2) + (fun opt2 -> opt2) + (obj8 + (opt "answers_with_loc" bool) + (opt "frontend" frontend_encoding) + (opt "input_format" format_encoding) + (opt "parse_only" bool) + (opt "parsers" (list string)) + (opt "preludes" (list string)) + (opt "type_only" bool) + (opt "type_smt2" bool) + ) + +let opt3_encoding = + conv + (fun opt3 -> opt3) + (fun opt3 -> opt3) + (obj8 + (opt "disable_weaks" bool) + (opt "enable_assertions" bool) + (opt "age_bound" int31) + (opt "fm_cross_limit" int31) + (opt "steps_bound" int31) + (opt "interpretation" int31) + (opt "output_format" format_encoding) + (opt "unsat_core" bool) + ) + +let opt4_encoding = + conv + (fun opt4 -> opt4) + (fun opt4 -> opt4) + (obj9 + (opt "verbose" bool) + (opt "instantiation_heuristic" instantiation_heuristic_encoding) + (opt "instanciate_after_backjump" bool) + (opt "max_multi_triggers_size" int31) + (opt "nb_triggers" int31) + (opt "no_ematching" bool) + (opt "no_user_triggers" bool) + (opt "normalize_instances" bool) + (opt "triggers_var" bool) + ) + +let opt5_encoding = + conv + (fun opt5 -> opt5) + (fun opt5 -> opt5) + (obj10 + (opt "arith_matchin" bool) + (opt "bottom_classes" bool) + (opt "cdcl_tableaux_inst" bool) + (opt "cdcl_tableaux_th" bool) + (opt "disable_flat_formulas_simplifiaction" bool) + (opt "enable_restarts" bool) + (opt "minimal_bj" bool) + (opt "no_backjumping" bool) + (opt "no_backward" bool) + (opt "no_decisions" bool) + ) + +let opt6_encoding = + conv + (fun opt6 -> opt6) + (fun opt6 -> opt6) + (obj10 + (opt "no_decisions_on" (list string)) + (opt "no_sat_learning" bool) + (opt "sat_solver" sat_solver_encoding) + (opt "tableaux_cdcl" bool) + (opt "disable_ites" bool) + (opt "inline_lets" bool) + (opt "rewriting" bool) + (opt "term_like_pp" bool) + (opt "disable_adts" bool) + (opt "no_ac" bool) + ) + +let opt7_encoding = + conv + (fun opt7 -> opt7) + (fun opt7 -> opt7) + (obj10 + (opt "no_contracongru" bool) + (opt "no_fm" bool) + (opt "no_nla" bool) + (opt "no_tcp" bool) + (opt "no_theory" bool) + (opt "restricted" bool) + (opt "tighten_vars" bool) + (opt "use_fpa" bool) + (opt "timers" bool) + (opt "file" string) + ) + +let options_encoding = + merge_objs opt_dbg1_encoding + (merge_objs opt_dbg2_encoding + (merge_objs opt_dbg3_encoding + (merge_objs opt1_encoding + (merge_objs opt2_encoding + (merge_objs opt3_encoding + (merge_objs opt4_encoding + (merge_objs opt5_encoding + (merge_objs opt6_encoding + opt7_encoding)))))))) + +let options_to_json opt = + let dbg_opt1 = + (opt.debug, + opt.debug_ac, + opt.debug_adt, + opt.debug_arith, + opt.debug_arrays, + opt.debug_bitv, + opt.debug_cc, + opt.debug_combine, + opt.debug_constr, + opt.debug_explanations) + in + let dbg_opt2 = + (opt.debug_fm, + opt.debug_fpa, + opt.debug_gc, + opt.debug_interpretation, + opt.debug_ite, + opt.debug_matching, + opt.debug_sat, + opt.debug_split, + opt.debug_sum, + opt.debug_triggers) + in + let dbg_opt3 = + (opt.debug_types, + opt.debug_typing, + opt.debug_uf, + opt.debug_unsat_core, + opt.debug_use, + opt.debug_warnings) + in + let all_opt1 = + (opt.rule, + opt.case_split_policy, + opt.enable_adts_cs, + opt.max_split, + opt.replay, + opt.replay_all_used_context, + opt.replay_used_context, + opt.save_used_context) + in + let all_opt2 = + (opt.answers_with_loc, + opt.frontend, + opt.input_format, + opt.parse_only, + opt.parsers, + opt.preludes, + opt.type_only, + opt.type_smt2) + in + let all_opt3 = + (opt.disable_weaks, + opt.enable_assertions, + opt.age_bound, + opt.fm_cross_limit, + opt.steps_bound, + opt.interpretation, + opt.output_format, + opt.unsat_core) + in + let all_opt4 = + (opt.verbose, + opt.instantiation_heuristic, + opt.instantiate_after_backjump, + opt.max_multi_triggers_size, + opt.nb_triggers, + opt.no_ematching, + opt.no_user_triggers, + opt.normalize_instances, + opt.triggers_var) + in + let all_opt5 = + (opt.arith_matching, + opt.bottom_classes, + opt.cdcl_tableaux_inst, + opt.cdcl_tableaux_th, + opt.disable_flat_formulas_simplification, + opt.enable_restarts, + opt.minimal_bj, + opt.no_backjumping, + opt.no_backward, + opt.no_decisions) + in + let all_opt6 = + (opt.no_decisions_on, + opt.no_sat_learning, + opt.sat_solver, + opt.tableaux_cdcl, + opt. disable_ites, + opt.inline_lets, + opt.rewriting, + opt.term_like_pp, + opt.disable_adts, + opt.no_ac) + in + let all_opt7 = + (opt.no_contracongru, + opt.no_fm, + opt.no_nla, + opt.no_tcp, + opt.no_theory, + opt.restricted, + opt.tighten_vars, + opt.use_fpa, + opt.timers, + opt.file) + in + let json_all_options = Json.construct options_encoding + (dbg_opt1, + (dbg_opt2, + (dbg_opt3, + (all_opt1, + (all_opt2, + (all_opt3, + (all_opt4, + (all_opt5, + (all_opt6, + all_opt7))))))))) + in + Js.string (Json.to_string json_all_options) + +let options_from_json options = + match Json.from_string (Js.to_string options) with + | Ok opts -> + let (dbg_opt1, + (dbg_opt2, + (dbg_opt3, + (all_opt1, + (all_opt2, + (all_opt3, + (all_opt4, + (all_opt5, + (all_opt6, + all_opt7))))))))) = Json.destruct options_encoding opts in + let (debug, + debug_ac, + debug_adt, + debug_arith, + debug_arrays, + debug_bitv, + debug_cc, + debug_combine, + debug_constr, + debug_explanations) = + dbg_opt1 in + let (debug_fm, + debug_fpa, + debug_gc, + debug_interpretation, + debug_ite, + debug_matching, + debug_sat, + debug_split, + debug_sum, + debug_triggers) = dbg_opt2 in + let (debug_types, + debug_typing, + debug_uf, + debug_unsat_core, + debug_use, + debug_warnings) = dbg_opt3 in + let (rule, + case_split_policy, + enable_adts_cs, + max_split, + replay, + replay_all_used_context, + replay_used_context, + save_used_context) = all_opt1 in + let (answers_with_loc, + frontend, + input_format, + parse_only, + parsers, + preludes, + type_only, + type_smt2) = all_opt2 in + let (disable_weaks, + enable_assertions, + age_bound, + fm_cross_limit, + steps_bound, + interpretation, + output_format, + unsat_core) = all_opt3 in + let (verbose, + instantiation_heuristic, + instantiate_after_backjump, + max_multi_triggers_size, + nb_triggers, + no_ematching, + no_user_triggers, + normalize_instances, + triggers_var) = all_opt4 in + let (arith_matching, + bottom_classes, + cdcl_tableaux_inst, + cdcl_tableaux_th, + disable_flat_formulas_simplification, + enable_restarts, + minimal_bj, + no_backjumping, + no_backward, + no_decisions) = all_opt5 in + let (no_decisions_on, + no_sat_learning, + sat_solver, + tableaux_cdcl, + disable_ites, + inline_lets, + rewriting, + term_like_pp, + disable_adts, + no_ac) = all_opt6 in + let (no_contracongru, + no_fm, + no_nla, + no_tcp, + no_theory, + restricted, + tighten_vars, + use_fpa, + timers, + file) = all_opt7 in + { + debug; + debug_ac; + debug_adt; + debug_arith; + debug_arrays; + debug_bitv; + debug_cc; + debug_combine; + debug_constr; + debug_explanations; + debug_fm; + debug_fpa; + debug_gc; + debug_interpretation; + debug_ite; + debug_matching; + debug_sat; + debug_split; + debug_sum; + debug_triggers; + debug_types; + debug_typing; + debug_uf; + debug_unsat_core; + debug_use; + debug_warnings; + rule; + case_split_policy; + enable_adts_cs; + max_split; + replay; + replay_all_used_context; + replay_used_context; + save_used_context; + answers_with_loc; + frontend; + input_format; + parse_only; + parsers; + preludes; + type_only; + type_smt2; + disable_weaks; + enable_assertions; + age_bound; + fm_cross_limit; + steps_bound; + interpretation; + output_format; + unsat_core; + verbose; + instantiation_heuristic; + instantiate_after_backjump; + max_multi_triggers_size; + nb_triggers; + no_ematching; + no_user_triggers; + normalize_instances; + triggers_var; + arith_matching; + bottom_classes; + cdcl_tableaux_inst; + cdcl_tableaux_th; + disable_flat_formulas_simplification; + enable_restarts; + minimal_bj; + no_backjumping; + no_backward; + no_decisions; + no_decisions_on; + no_sat_learning; + sat_solver; + tableaux_cdcl; + disable_ites; + inline_lets; + rewriting; + term_like_pp; + disable_adts; + no_ac;no_contracongru; + no_fm; + no_nla; + no_tcp; + no_theory; + restricted; + tighten_vars; + use_fpa; + timers; + file + } + | Error _e -> assert false + +type used_axiom = + | Used + | Unused + | Unknown + +let used_axiom_encoding = + union [ + case(Tag 1) + ~title:"Used" + (constant "Used") + (function Used -> Some () | _ -> None) + (fun () -> Used); + case(Tag 2) + ~title:"Unused" + (constant "Unused") + (function Unused -> Some () | _ -> None) + (fun () -> Unused); + case(Tag 3) + ~title:"Unknown" + (constant "Unknown") + (function Unknown -> Some () | _ -> None) + (fun () -> Unknown); + ] + +type statistics = + (string * int * int * int * used_axiom) list + +let statistics_encoding = + list (tup5 string int31 int31 int31 used_axiom_encoding) + +type status = + | Unsat of int + | Inconsistent of int + | Sat of int + | Unknown of int + | LimitReached of string + | Error of string + +let status_encoding = + union [ + case(Tag 1) + ~title:"Unsat" + (obj1 (req "Unsat" int31)) + (function Unsat n -> Some n | _ -> None) + (fun n -> Unsat(n)); + case(Tag 2) + ~title:"Inconsistent" + (obj1 (req "Inconsistent" int31)) + (function Inconsistent n -> Some n | _ -> None) + (fun n -> Inconsistent(n)); + case(Tag 3) + ~title:"Sat" + (obj1 (req "Sat" int31)) + (function Sat n -> Some n | _ -> None) + (fun n -> Sat(n)); + case(Tag 4) + ~title:"Unknown" + (obj1 (req "Unknown" int31)) + (function Unknown n -> Some n | _ -> None) + (fun n -> Unknown(n)); + case(Tag 5) + ~title:"LimitReached" + (obj1 (req "LimitReached" string)) + (function LimitReached s -> Some s | _ -> None) + (fun s -> LimitReached(s)); + case(Tag 6) + ~title:"Error" + (obj1 (req "Error" string)) + (function Error s -> Some s | _ -> None) + (fun s -> Error(s)); + ] + +type results = { + worker_id : int option; + status : status; + results : string list option; + errors : string list option; + warnings : string list option; + debugs : string list option; + statistics : statistics option; + model : string list option; + unsat_core : string list option; +} + +let init_results () = { + worker_id = None; + status = Unknown (-1); + results = None; + errors = None; + warnings = None; + debugs = None; + statistics = None; + model = None; + unsat_core = None; +} + +let results_encoding = + conv + (fun {worker_id; status; results; errors; warnings; + debugs; statistics; model; unsat_core } -> + (worker_id, status, results, errors, warnings, + debugs, statistics, model, unsat_core)) + (fun (worker_id, status, results, errors, warnings, + debugs, statistics, model, unsat_core) -> + {worker_id; status; results; errors; warnings; + debugs; statistics; model; unsat_core }) + (obj9 + (opt "worker_id" int31) + (req "status" status_encoding) + (opt "results" (list string)) + (opt "errors" (list string)) + (opt "warnings" (list string)) + (opt "debugs" (list string)) + (opt "statistics" statistics_encoding) + (opt "model" (list string)) + (opt "unsat_core" (list string))) + +let results_to_json res = + let json_results = Json.construct results_encoding res in + Js.string (Json.to_string json_results) + +let results_from_json res = + match Json.from_string (Js.to_string res) with + | Ok res -> Json.destruct results_encoding res + | Error _e -> assert false + + +let file_encoding = + conv + (fun f -> f) + (fun f -> f) + (obj3 + (opt "filename" string) + (opt "worker_id" int31) + (req "content" (list string))) + +let file_to_json filename worker_id content = + let json_file = Json.construct file_encoding (filename,worker_id,content) in + Js.string (Json.to_string json_file) + +let file_from_json res = + match Json.from_string (Js.to_string res) with + | Ok res -> Json.destruct file_encoding res + | Error _e -> assert false diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli new file mode 100644 index 000000000..382216b2d --- /dev/null +++ b/src/bin/js/worker_interface.mli @@ -0,0 +1,229 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +(** {1 Worker interface module} *) + +(** This module aims to facilitate the exhanges from/to the Alt-Ergo's worker *) + +(** {2 Option types} *) + +(** Types extract from AltErgoLib Utils.util and Utils.options usefull for + interact with the worker *) + +type input_format = Native | Smtlib2 | Why3 (* | SZS *) | Unknown of string +type output_format = input_format + +type case_split_policy = + | AfterTheoryAssume (* default *) + | BeforeMatching + | AfterMatching + +type sat_solver = + | Tableaux + | Tableaux_CDCL + | CDCL + | CDCL_Tableaux + +type frontend = + | Legacy + | Unknown of string + +type instantiation_heuristic = INormal | IAuto | IGreedy + +(** Record type that contains all options that can be set for the Alt-Ergo's + worker. *) +type options = { + debug : bool option; + debug_ac : bool option; + debug_adt : bool option; + debug_arith : bool option; + debug_arrays : bool option; + debug_bitv : bool option; + debug_cc : bool option; + debug_combine : bool option; + debug_constr : bool option; + debug_explanations : bool option; + debug_fm : bool option; + debug_fpa : int option; + debug_gc : bool option; + debug_interpretation : bool option; + debug_ite : bool option; + debug_matching : int option; + debug_sat : bool option; + debug_split : bool option; + debug_sum : bool option; + debug_triggers : bool option; + debug_types : bool option; + debug_typing : bool option; + debug_uf : bool option; + debug_unsat_core : bool option; + debug_use : bool option; + debug_warnings : bool option; + rule : int option; + + case_split_policy : case_split_policy option; + enable_adts_cs : bool option; + max_split : int option; + + replay : bool option; + replay_all_used_context : bool option; + replay_used_context : bool option; + save_used_context : bool option; + + answers_with_loc : bool option; + frontend : frontend option; + input_format : input_format option; + parse_only : bool option; + parsers : (string list) option; + preludes : (string list) option; + type_only : bool option; + type_smt2 : bool option; + + disable_weaks : bool option; + enable_assertions : bool option; + + age_bound : int option; + fm_cross_limit : int option; + steps_bound : int option; + + interpretation : int option; + + output_format : output_format option; + unsat_core : bool option; + + + verbose : bool option; + + instantiation_heuristic : instantiation_heuristic option; + instantiate_after_backjump : bool option; + max_multi_triggers_size : int option; + nb_triggers : int option; + no_ematching : bool option; + no_user_triggers : bool option; + normalize_instances : bool option; + triggers_var : bool option; + + arith_matching : bool option; + bottom_classes : bool option; + cdcl_tableaux_inst : bool option; + cdcl_tableaux_th : bool option; + disable_flat_formulas_simplification : bool option; + enable_restarts : bool option; + minimal_bj : bool option; + no_backjumping : bool option; + no_backward : bool option; + no_decisions : bool option; + no_decisions_on : (string list) option; + no_sat_learning : bool option; + sat_solver : sat_solver option; + tableaux_cdcl : bool option; + + disable_ites : bool option; + inline_lets : bool option; + rewriting : bool option; + term_like_pp : bool option; + + disable_adts : bool option; + no_ac : bool option; + no_contracongru : bool option; + no_fm : bool option; + no_nla : bool option; + no_tcp : bool option; + no_theory : bool option; + restricted : bool option; + tighten_vars : bool option; + use_fpa : bool option; + timers : bool option; + + file : string option; +} + +type used_axiom = + | Used + | Unused + | Unknown + +(** type that contains a list of the axiom used in instances. + axiom name, start pos, end pos, number of time its used in insstances, + Used if its usefull to solve the goal (from unsat core), Unused otherwise + Unknown if the unsat-core option is not setted *) +type statistics = + (string * int * int * int * used_axiom) list + +(** Type used to return the status of solving + This can be usefull to match status instead of analysing + results and errors fields *) +type status = + | Unsat of int + | Inconsistent of int + | Sat of int + | Unknown of int + | LimitReached of string + | Error of string + +(** Record type that contains all results that can be returned by the + Alt-Ergo's worker. *) +type results = { + worker_id : int option; + status : status; + results : string list option; + errors : string list option; + warnings : string list option; + debugs : string list option; + statistics : statistics option; + model : string list option; + unsat_core : string list option; +} + +(** {2 Functions} *) + +(** {3 File functions} *) + +(** Take an optional file name, an optional worker identifier (integer) and + the file content as a string and convert + it to a json file into Js string *) +val file_to_json : + string option -> int option -> string list -> + Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t + +(** Take a Js string corresponding to a Json file and decoding in into + an optional file name, an optional worker identifier and the file content *) +val file_from_json : + Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t -> + string option * int option * string list + +(** {3 Options functions} *) + +(** Return a record containing None for all options in the option type + Since the function set_options in options_interface set only options + with value (Some v), this function is use to create a record with all + field to None. *) +val init_options : unit -> options + +(** Return a JS string correspondind of the encoding in Json of the options. + Field with None value or not included in the Json.*) +val options_to_json : options -> Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t + +(** Get a JS string corresponding of a Json and decoding it into a record of + the options type. If some field are not included in the Json, + the value None is set for this fields *) +val options_from_json : Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t -> options + +(** {3 Results functions} *) + +(** Return a record containing None for all results field in the results type *) +val init_results : unit -> results + +(** Convert the results type to Json into a Js string *) +val results_to_json : results -> Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t + +(** Convert Js string corresponding to a Json file into the results type *) +val results_from_json : Js_of_ocaml.Js.js_string Js_of_ocaml.Js.t -> results diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml new file mode 100644 index 000000000..aa49ab701 --- /dev/null +++ b/src/bin/js/worker_js.ml @@ -0,0 +1,256 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2018-2020 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +open Js_of_ocaml +open Js_of_ocaml_lwt +open Alt_ergo_common +open AltErgoLib + +(* Internal state while iterating over input statements *) +type 'a state = { + env : 'a; + ctx : Commands.sat_tdecl list; + local : Commands.sat_tdecl list; + global : Commands.sat_tdecl list; +} + +(* If the buffer is not empty split the string in strings at each newline *) +let check_buffer_content b = + let buf_cont = Buffer.contents b in + if String.equal buf_cont "" then + None + else + let buf = String.split_on_char '\n' buf_cont in + Some buf + +let check_context_content c = + match c with + | [] -> None + | _ -> Some c + +let main worker_id content = + + (* Create buffer for each formatter + The content of this buffers are then retrieved and send as results *) + let buf_std = Buffer.create 10 in + Options.set_fmt_std (Format.formatter_of_buffer buf_std); + let buf_err = Buffer.create 10 in + Options.set_fmt_err (Format.formatter_of_buffer buf_err); + let buf_wrn = Buffer.create 10 in + Options.set_fmt_wrn (Format.formatter_of_buffer buf_wrn); + let buf_dbg = Buffer.create 10 in + Options.set_fmt_dbg (Format.formatter_of_buffer buf_dbg); + let buf_mdl = Buffer.create 10 in + Options.set_fmt_mdl (Format.formatter_of_buffer buf_mdl); + let buf_usc = Buffer.create 10 in + Options.set_fmt_usc (Format.formatter_of_buffer buf_usc); + + (* Status updated regarding if AE succed or failed + (error or steplimit reached) *) + let returned_status = ref (Worker_interface.Unknown 0) in + + (* let context = ref ([],[]) in *) + let unsat_core = ref [] in + let tbl = Hashtbl.create 53 in + + + (* Initialisation *) + Input_frontend.register_legacy (); + + let module SatCont = + (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer) in + + let module TH = + (val + (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S) + else (module Theory.Main_Default : Theory.S)) : Theory.S ) in + + let module SAT = SatCont.Make(TH) in + + let module FE = Frontend.Make (SAT) in + + (* Aux function used to record axioms used in instantiations *) + let add_inst orig = + let id = Expr.uid orig in + begin + try incr (snd (Hashtbl.find tbl id)) + with Not_found -> Hashtbl.add tbl id (orig, ref 1) + end; + true + in + + let get_status_and_print status n = + returned_status := + begin match status with + | FE.Unsat _ -> Worker_interface.Unsat n + | FE.Inconsistent _ -> Worker_interface.Inconsistent n + | FE.Sat _ -> Worker_interface.Sat n + | FE.Unknown _ -> Worker_interface.Unknown n + | FE.Timeout _ -> Worker_interface.LimitReached "timeout" + | FE.Preprocess -> Worker_interface.Unknown n + end; + FE.print_status status n + in + + let solve all_context (cnf, goal_name) = + let used_context = FE.choose_used_context all_context ~goal_name in + let consistent_dep_stack = Stack.create () in + SAT.reset_refs (); + let _,_,dep = + List.fold_left + (FE.process_decl + get_status_and_print used_context consistent_dep_stack) + (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in + + if Options.get_unsat_core () then begin + unsat_core := Explanation.get_unsat_core dep; + end; + in + + let typed_loop all_context state td = + match td.Typed.c with + | Typed.TGoal (_, kind, name, _) -> + let l = state.local @ state.global @ state.ctx in + let cnf = List.rev @@ Cnf.make l td in + let () = solve all_context (cnf, name) in + begin match kind with + | Typed.Check + | Typed.Cut -> { state with local = []; } + | _ -> { state with global = []; local = []; } + end + | Typed.TAxiom (_, s, _, _) when Typed.is_global_hyp s -> + let cnf = Cnf.make state.global td in + { state with global = cnf; } + | Typed.TAxiom (_, s, _, _) when Typed.is_local_hyp s -> + let cnf = Cnf.make state.local td in + { state with local = cnf; } + | _ -> + let cnf = Cnf.make state.ctx td in + { state with ctx = cnf; } + in + + let (module I : Input.S) = Input.find (Options.get_frontend ()) in + let parsed () = + try + Options.Time.start (); + Options.set_is_gui false; + I.parse_file ~content ~format:None + with + | Parsing.Parse_error -> + Printer.print_err "%a" Errors.report + (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),"")); + raise Exit + | Errors.Error e -> + begin match e with + | Errors.Run_error r -> begin + match r with + | Steps_limit _ -> + returned_status := + Worker_interface.LimitReached "Steps limit" + | _ -> returned_status := Worker_interface.Error "Run error" + end + | _ -> returned_status := Worker_interface.Error "Error" + end; + Printer.print_err "%a" Errors.report e; + raise Exit + in + let all_used_context = FE.init_all_used_context () in + let assertion_stack = Stack.create () in + let typing_loop state p = + try + let l, env = I.type_parsed state.env assertion_stack p in + List.fold_left (typed_loop all_used_context) { state with env; } l + with Errors.Error e -> + Printer.print_err "%a" Errors.report e; + raise Exit + in + + let state = { + env = I.empty_env; + ctx = []; + local = []; + global = []; + } in + + begin + try let _ : _ state = + Seq.fold_left typing_loop state (parsed ()) in () + with Exit -> () end; + + let compute_statistics () = + let used = + List.fold_left (fun acc ({Explanation.f;_} as r) -> + Util.MI.add (Expr.uid f) r acc + ) Util.MI.empty (!unsat_core) in + Hashtbl.fold (fun id (f,nb) acc -> + match Util.MI.find_opt id used with + | None -> begin + match Expr.form_view f with + | Lemma {name=name;loc=loc;_} -> + let b,e = loc in + let used = + if Options.get_unsat_core () then Worker_interface.Unused + else Worker_interface.Unknown in + (name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,used) :: acc + | _ -> acc + end + | Some r -> + let b,e = r.loc in + (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,Worker_interface.Used) + :: acc + ) tbl [] + in + + + (* returns a records with compatible worker_interface fields *) + { + Worker_interface.worker_id = worker_id; + Worker_interface.status = !returned_status; + Worker_interface.results = check_buffer_content buf_std; + Worker_interface.errors = check_buffer_content buf_err; + Worker_interface.warnings = check_buffer_content buf_wrn; + Worker_interface.debugs = check_buffer_content buf_dbg; + Worker_interface.statistics = + check_context_content (compute_statistics ()); + Worker_interface.model = check_buffer_content buf_mdl; + Worker_interface.unsat_core = check_buffer_content buf_usc; + } + + +(** Worker initialisation + Run Alt-ergo with the input file (string) + and the corresponding set of options + Return a couple of list for status (one per goal) and errors *) +let () = + Worker.set_onmessage (fun (json_file,json_options) -> + Lwt_js_events.async (fun () -> + let filename,worker_id,filecontent = + Worker_interface.file_from_json json_file in + begin match filename with + | Some fl -> Options.set_file_for_js fl + | None -> Options.set_file_for_js "" + end; + let filecontent = String.concat "\n" filecontent in + (* Format.eprintf + "file content : @, %s @,@, end of file @." filecontent; *) + + (* Extract options and set them *) + let options = Worker_interface.options_from_json json_options in + Options_interface.set_options options; + + (* Run the worker on the input file (filecontent) *) + let results = main worker_id filecontent in + + (* Convert results and returns them *) + Worker.post_message (Worker_interface.results_to_json results); + Lwt.return (); + ) + ) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 19df867fc..3807121ef 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -138,8 +138,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | None -> false | Some s -> not (Util.SS.mem name s) - let mk_root_dep f_name = - if Options.get_unsat_core () then Ex.singleton (Ex.RootDep f_name) + let mk_root_dep name f loc = + if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty let process_decl print_status used_context consistent_dep_stack @@ -161,7 +161,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if not is_hyp && unused_context n used_context then acc else - let dep = if is_hyp then Ex.empty else mk_root_dep n in + let dep = if is_hyp then Ex.empty else mk_root_dep n f d.st_loc in if consistent then SAT.assume env {E.ff=f; @@ -182,7 +182,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct | PredDef (f, name) -> if unused_context name used_context then acc else - let dep = mk_root_dep name in + let dep = mk_root_dep name f d.st_loc in SAT.pred_def env f name dep d.st_loc, consistent, dep | RwtDef _ -> assert false @@ -212,12 +212,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct print_status (Unsat (d, dep)) (Steps.get_steps ()); env, false, dep - | ThAssume ({ Expr.ax_name; _ } as th_elt) -> + | ThAssume ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) -> if unused_context ax_name used_context then acc else if consistent then - let dep = mk_root_dep ax_name in + let dep = mk_root_dep ax_name ax_form d.st_loc in let env = SAT.assume_th_elt env th_elt dep in env, consistent, dep else env, consistent, dep diff --git a/src/lib/frontend/input.ml b/src/lib/frontend/input.ml index 6631745ff..0de01f09a 100644 --- a/src/lib/frontend/input.ml +++ b/src/lib/frontend/input.ml @@ -17,6 +17,8 @@ module type S = sig type parsed + val parse_file : content:string -> format:string option -> parsed Seq.t + val parse_files : filename:string -> preludes:string list -> parsed Seq.t diff --git a/src/lib/frontend/input.mli b/src/lib/frontend/input.mli index 45b014d0d..90ea3ef12 100644 --- a/src/lib/frontend/input.mli +++ b/src/lib/frontend/input.mli @@ -34,6 +34,9 @@ module type S = sig type parsed (** The type of a parsed statement. *) + val parse_file : content:string -> format:string option -> parsed Seq.t + (** Parse a file as a string with the given format or the input_format set *) + val parse_files : filename:string -> preludes:string list -> parsed Seq.t (** Parse a file (and some preludes). *) diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index e5a815717..2fd6c6a9c 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -53,6 +53,8 @@ module type S = sig [f] is unsatisfiable in [env] *) val assume : t -> Expr.gformula -> Explanation.t -> t + (** [assume env f exp] assume a new formula [f] with the explanation [exp] + in the theories environment of [env]. *) val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t (** [pred_def env f] assume a new predicate definition [f] in [env]. *) @@ -63,6 +65,8 @@ module type S = sig [size]. Raises Sat if [f] is satisfiable in [env] *) val unsat : t -> Expr.gformula -> Explanation.t + (** [print_model header fmt env] print propositional model and theory model + on the corresponding fmt. *) val print_model : header:bool -> Format.formatter -> t -> unit val reset_refs : unit -> unit diff --git a/src/lib/structures/explanation.ml b/src/lib/structures/explanation.ml index 53d137db6..f6bb19dee 100644 --- a/src/lib/structures/explanation.ml +++ b/src/lib/structures/explanation.ml @@ -30,12 +30,14 @@ open Format module E = Expr +type rootdep = { name : string; f : Expr.t; loc : Loc.t} + type exp = | Literal of Satml_types.Atom.atom | Fresh of int | Bj of E.t | Dep of E.t - | RootDep of string (* name of the toplevel formula *) + | RootDep of rootdep module S = Set.Make @@ -45,7 +47,7 @@ module S = | Fresh i1, Fresh i2 -> i1 - i2 | Literal a , Literal b -> Satml_types.Atom.cmp_atom a b | Dep e1 , Dep e2 -> E.compare e1 e2 - | RootDep s, RootDep t -> String.compare s t + | RootDep r1, RootDep r2 -> E.compare r1.f r2.f | Bj e1 , Bj e2 -> E.compare e1 e2 | Literal _, _ -> -1 @@ -112,18 +114,27 @@ let print fmt ex = | Literal a -> fprintf fmt "{Literal:%a}, " Satml_types.Atom.pr_atom a | Fresh i -> Format.fprintf fmt "{Fresh:%i}" i; | Dep f -> Format.fprintf fmt "{Dep:%a}" E.print f - | RootDep s -> Format.fprintf fmt "{RootDep:%s}" s + | RootDep r -> Format.fprintf fmt "{RootDep:%s}" r.name | Bj f -> Format.fprintf fmt "{BJ:%a}" E.print f ) ex; fprintf fmt "}" end +let get_unsat_core dep = + fold_atoms + (fun a acc -> + match a with + | RootDep r -> r :: acc + | Dep _ -> acc + | Bj _ | Fresh _ | Literal _ -> assert false + ) dep [] + let print_unsat_core ?(tab=false) fmt dep = iter_atoms (function - | RootDep s -> - if tab then Format.fprintf fmt " %s@." s (* tab is too big *) - else Format.fprintf fmt "%s@." s + | RootDep r -> + if tab then Format.fprintf fmt " %s@." r.name (* tab is too big *) + else Format.fprintf fmt "%s@." r.name | Dep _ -> () | Bj _ | Fresh _ | Literal _ -> assert false ) dep diff --git a/src/lib/structures/explanation.mli b/src/lib/structures/explanation.mli index 37ef57d81..d840300f8 100644 --- a/src/lib/structures/explanation.mli +++ b/src/lib/structures/explanation.mli @@ -28,12 +28,13 @@ type t +type rootdep = { name : string; f : Expr.t; loc : Loc.t} type exp = | Literal of Satml_types.Atom.atom | Fresh of int | Bj of Expr.t | Dep of Expr.t - | RootDep of string (* name of the toplevel formula *) + | RootDep of rootdep exception Inconsistent of t * Expr.Set.t list @@ -66,6 +67,8 @@ val add_fresh : exp -> t -> t val print : Format.formatter -> t -> unit +val get_unsat_core : t -> rootdep list + val print_unsat_core : ?tab:bool -> Format.formatter -> t -> unit val formulas_of : t -> Expr.Set.t diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index d1d237a1e..12b6700e2 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -26,20 +26,23 @@ (* *) (******************************************************************************) -(* Global formatter declarations and setters, can't be directly used *) -let std_fmt = ref Format.std_formatter -let err_fmt = ref Format.err_formatter - -let set_std_fmt f = std_fmt := f -let set_err_fmt f = err_fmt := f - (* Formatter declarations, getters and setters *) -let fmt_std = std_fmt -let fmt_err = err_fmt -let fmt_wrn = err_fmt -let fmt_dbg = err_fmt -let fmt_mdl = std_fmt -let fmt_usc = std_fmt +let fmt_std = ref Format.std_formatter +let fmt_err = ref Format.err_formatter +let fmt_wrn = ref Format.err_formatter +let fmt_dbg = ref Format.err_formatter +let fmt_mdl = ref Format.std_formatter +let fmt_usc = ref Format.std_formatter + +let set_std_fmt f = + fmt_std := f; + fmt_mdl := f; + fmt_usc := f + +let set_err_fmt f = + fmt_err := f; + fmt_wrn := f; + fmt_dbg := f let get_fmt_std () = !fmt_std let get_fmt_err () = !fmt_err diff --git a/src/parsers/parsers.ml b/src/parsers/parsers.ml index c02d1253c..d2eef05b9 100644 --- a/src/parsers/parsers.ml +++ b/src/parsers/parsers.ml @@ -170,3 +170,12 @@ let parse_problem ~filename ~preludes = in List.rev_append (List.rev (parse_input_file prelude)) acc) acc (List.rev preludes) + +let parse_problem_as_string ~content ~format = + Parsers_loader.load (); + try + let lb = Lexing.from_string content in + parse_file ?lang:format lb + with + | Errors.Error e -> raise (Error e) + | Parsing.Parse_error as e -> raise e diff --git a/src/parsers/parsers.mli b/src/parsers/parsers.mli index 001206a58..5d0cfd14c 100644 --- a/src/parsers/parsers.mli +++ b/src/parsers/parsers.mli @@ -65,3 +65,10 @@ val parse_problem : filename:string -> preludes:string list -> Parsed.file chosen depending on the extension of different files. @raise Errors.Error @raise Parsing.Parse_Error *) + +val parse_problem_as_string : + content:string -> format:string option -> Parsed.file +(** Parses the given input file as a string. + Parser is chosen depending on the given format or the input_format set. + @raise Errors.Error + @raise Parsing.Parse_Error *)