GitLab

If drivers in why3.conf are simple names like "alt_ergo", then the driver file
is search as <datadir>/drivers/alt_ergo.drv

This behavior is now the same as when a driver is given with option -D on the
command line for why3prove, why3replay or why3extract

Reminder: the datadir is either given as
1) the environment variable WHY3DATA
2) the field "datadir" of the [main] section of the
   why3 config file if exists
3) or by default the compile-time datadir

This is more convenient when using only the Why3 API from SPARK for
example.

Parsing reference was forgotten in commit for Q217-025. This solves the
problem with a new token MK_ANYTHING.

* src/driver/parse_smtv2_model_lexer.mll
(parse): Added lexing for all remaining mk*___ record constructs.

* src/driver/parse_smtv2_model_parser.mly
(smt_term): An smt_term can be a reference to a smt_term. It means it can
be (Mk_anything smt_term).

Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5

Do not print (get-info :reason-unknown) on smt2 output. Previously,
detection of end of model and beginning of statistics was done by using
the reason. We now detect a single parenthesis on a line: every cvc4 model
ends with this (we assume statistics does not contain a line beginning
with a closing parenthesis). As a side effect, we also find
more counterexamples.

* src/driver/parse_smtv2_model.ml
(parse): Revert changes that were detecting Abort trap.

* src/driver/parse_smtv2_model_parser.mly
(output): Revert changes to allow absence of parenthesis at the end. Also
removed parsing on results given by the reason. Now match on ).

* src/printer/smtv2_cvc_ce.ml
(print_prop_decl): Remove (get-info :reason-unknown).

* src/printer/smtv2.ml
(print_prop_decl): Remove get-info for coherence.

Change-Id: Ifbd7b2b9ce499f8aaa020f58375d784793990965

This patch allows parsing model including the error message raised by cvc4
on mac.

* src/driver/parse_smtv2_model.ml
(parse): Allow parsing of specific error message "Abort trap".
(output): Allow parsing when last parenthesis is missing which is the case
when the bug is occuring.

Change-Id: I80d7276d37916e09ba4bb28478ac9a7427789771

Change-Id: Id165717756375db150031589740470cc1e08b8ac

This commit solves a CVC4 limitation on boolean inside datatypes for CE.
It converts them to bv by adding a new printer. This commit is a hack and
it will be reverted when the bug is solved in CVC4.

* Makefile.in
(Makefile): Added new printer.
* drivers/smtv-libv2_cvc_ce.drv:
(printer): new printer used is smtv2_cvc_ce
* src/driver/parse_smtv2_model_lexer.mll
(parse): Changed the way constructor of datatype are detected.
* src/printer/smtv2_cvc_ce.ml
(print_constructors): Projections to bool are changed to projections
to bitvectors. Duplicate projections are generated which returns bool and
are used in the rest of smtv2 generated.

Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881

This commit allows parsing of the result of get-model from smtsolvers.
It changes the communication between why3 and Spark for CE to communicate
records and array as JSON values.

 * src/core/model_parser.ml
(model_value): Adding boolean and record type to model values.
(print_*): Changed printing functions to print arrays and records as JSON
values not as strings.

 * src/driver/collect_data_model.ml
(get_variables_*): collect all internal variables of a term and put them
into a map.
(add_all_cvc): Add all cvc4 variables in the model to a global map.
(add_vars_to_table): Add values of variables that can be deduced from ITE
 to the table.
(corres_else_element): Take the definitions of functions to_rep/of_rep
and extract the values of internal CVC variables from it.
(refine_*): Recursively replace internal variables in a term with values
taken from the table.
(convert_*): Convert to type model_value from model_parser.ml.
(create_list): Combine the following to get a list of model_value from
the parsing of the model.

* src/driver/parse_smtv2_model.ml
(parse): Changed the detected end of model.

* src/driver/parse_smtv2_model_lexer.mll
(rule): Added tokens related to model definitions and SPARK definitions of
records, discriminants and ref.

* src/driver/parse_smtv2_model_parser.mly
(output): Changed the parser so that it can parse a model as returned by
Cvc4 or z3.

* src/driver/smt2_model_defs.ml
(print_*): Added printing functions for terms.
(make_local*): Changes the AST of terms to differentiate smtsolver
internal variables, user-defined variables and local variables.
(subst*): Removes the local let bindings introduced by z3.
(build_record_discr): Put definitions of discriminants inside the record
definition.

 * src/printer/smtv2.ml
(print_logic_decl): Removed get-values and added get-model.

* src/transform/intro_projections_counterexmp.ml
(intro_const_equal_to_term): Only allow projections for attributes first,
last and field projections. Necessary when the field of a record is
itself on array on which we want to get First and Last.

* src/transform/intro_vc_vars_counterexmp.ml
(do_intro): Some definitions moved to intro_projections_counterexmp.ml.

Change-Id: Ib77fb66a2f7c53a9f54cfc300c8984e1fcec8087

* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.

Add a name_table in printer_args.
Put the definition of name_table in task.ml.
Build_name_tables only called once in proof_node creation.
Modified the rest accordingly.

* call_provers.ml
(prover_update): Adding unimplemented errors that reflects the cases of
proof_attempt_status. Otherwise, proof_attempt_status is a list of cases
that are never reached.
* controller_itp.ml
(proof_attempt_status): Added Uninstalled case in proof_attempt_status.
Launched in replay when asked to replay something not installed.
(print_trans_status): Adding a ! when proof is valid for debugging
reasons.
(report): Added a report type for replay reporting of differences.
(print_report): printing function for report.
(replay_print): callback used with replay to print the report at the end.
(replay): Function that replays all proof attempts of the session.

* session_itp.ml
(session_iter_proof_attempt): Added the proofNodeID the fold function
for convenience.
* why3shell.ml
(test_replay): Added to test replay.

Sometimes the windows syscall GetExitCodeProcess returns a large result,
larger than the ocaml [int] type. This is expected and not an error. For
example the constant STATUS_QUOTA_EXCEEDED, which is 0xC0000044, may be
a valid exit code. Such large values trip up the [int_of_string] parsing
in the client.

This patch implements the following solution to this problem:
* the server doesn't care and sends the large value;
* (the server now recognizes this value, though, to set the timeout flag
  more often)
* the client uses an Int64 value to parse that big constant;
* when converting to the internal Unix.process_status type, we simply
  convert to [int], because such large values don't have any special
  meaning for Why3 anyway.

* call_provers.ml
(parse_prover_run): now directly take the exit status as argument, and
convert it to int;
(handle_answer): don't wrap argument to parse_prover_run into unix type
* prove_client.ml
(read_answer): read Int64 type now
* server-win.c
(handle_child_event): set timeout boolean also when exitcode is equal to
   constant STATUS_QUOTA_EXCEEDED

Change-Id: I1163a6f1adf1bdbfe1f53269ce0ae57dc8bd0287

- Call_provers.parse_prover_run does not attempt fixing answer anymore,
  except in the case where the answer is HighFailure and time is close
  to time limit (which is considered as Timeout)

- Session_scheduler.fuzzy_proof_time is now more liberal, accepts
  that two answers Unknown or Timeout of OutOfMemory with less than
  10% difference in time are equivalent, and thus should not be
  reported as a significant change

Adding "I don't know" as a correct keyword for provers return (inside
counterexamples).
Updating scripts because of move from hoare_logic to WP_revisited.

* src/driver/parse_smtv2_model.ml
(parse): Adding I dont know as a keyword.

* bench/bench
Changing to WP_revisited.

* examples/bench.sh
Changing to WP_revisited.

* examples/regtests.sh
Changing to WP_revisited.

add exception handler for int_of_string failure and raise the correct
exception here

We added the generation of identifiers for counterex values inside the
printer of altergo.
Also added a file to factorize counterex printing functions that are used
for both altergo and smtv2.

* Makefile.in
(cntexmp_printer): Factorization file added to Makefile.

* src/driver/parse_smtv2_model_lexer.mll
(MODEL): Adding model keyword.

* src/driver/parse_smtv2_model_parser.mly
(output): Added parsing when keyword model is at beginning of the
 output of the prover.

* src/printer/alt_ergo.ml
Adding info mimicking smtv2.ml inside most printing functions for counterex
generation.

* src/printer/cntexmp_printer.ml
Common functions to alt_ergo.ml and smtv2.ml

* src/printer/smtv2.ml
Removed functions that are factorized into cntexmp_printer.ml

this allows to account for the cumulative CPU time spent
in the dedicated server in the stats of the client process,
which is necessary to estimate correctly the execution
time of coqtop on proof scripts using the why3 tactic.

Also, make several connection attempts before giving up.

The adaptation of time limits was incorrect, and could transform "0" (no
time limit) to "1" (second).

* call_provers.ml
(adapt_limit): do nothing when no time limit was present

Call_provers:

- drop closures "pre_prover_call" and "post_prover_call". They were
  intended to be used for synchronous interaction with provers from
  multiple threads. This is now responsibility of the proof server:
  (a) any Call_prover.call_on_[file|buffer] submits the proof task
      immediately to the server;
  (b) all proof results are handled in the working Why3 thread.

- Call_provers.query_call returns a tri-state "prover_update" type
  which can be one of: "ProverStarted" (returned after the proof
  server informs Why3 that a prover was started), "ProverFinished"
  (returned after the proof server returns the prover result), and
  "NoUpdates" (returned when the proof server has not sent any new
  updates concerning the proof task in question).

    IMPORTANT: query_call does not maintain the state of a given
  prover call. In a normal use case, "ProverFinished" is returned
  _exactly_ once, and "ProverStarted" _at_most_ once (never for
  an editor call or when rapidly overwritten by "ProverFinished").

    TODO: extend the proof server protocol and implementation to
  send "ProverStarted" events back to Why3.