Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

1 files changed, 357 insertions, 0 deletions

diff --git a/src/lfsc/lfscLexer.mll b/src/lfsc/lfscLexer.mll
new file mode 100644
index 0000000..3e8d5f9
--- /dev/null
+++ b/src/lfsc/lfscLexer.mll
@@ -0,0 +1,357 @@
+{
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+(* This parser is adapted from Jane Street sexplib parser *)
+
+  open Printf
+  open Lexing
+  open LfscParser
+
+  let char_for_backslash = function
+    | 'n' -> '\010'
+    | 'r' -> '\013'
+    | 'b' -> '\008'
+    | 't' -> '\009'
+    | c -> c
+
+  let lf = '\010'
+
+  let dec_code c1 c2 c3 =
+    100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48)
+
+  let hex_code c1 c2 =
+    let d1 = Char.code c1 in
+    let val1 =
+      if d1 >= 97 then d1 - 87
+      else if d1 >= 65 then d1 - 55
+      else d1 - 48 in
+    let d2 = Char.code c2 in
+    let val2 =
+      if d2 >= 97 then d2 - 87
+      else if d2 >= 65 then d2 - 55
+      else d2 - 48 in
+    val1 * 16 + val2
+
+  let found_newline ({ lex_curr_p; _ } as lexbuf) diff =
+    lexbuf.lex_curr_p <-
+      {
+        lex_curr_p with
+        pos_lnum = lex_curr_p.pos_lnum + 1;
+        pos_bol = lex_curr_p.pos_cnum - diff;
+      }
+
+  (* same length computation as in [Lexing.lexeme] *)
+  let lexeme_len { lex_start_pos; lex_curr_pos; _ } = lex_curr_pos - lex_start_pos
+
+  let main_failure lexbuf msg =
+    let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_start_p lexbuf in
+    let msg =
+      sprintf
+        "Sexplib.Lexer.main: %s at line %d char %d"
+        msg pos_lnum (pos_cnum - pos_bol)
+    in
+    failwith msg
+
+  module type T = sig
+    module Quoted_string_buffer : sig
+      type t
+      val create : int -> t
+      val add_char : t -> char -> unit
+      val add_substring : t -> string -> int -> int -> unit
+      val add_lexeme : t -> lexbuf -> unit
+      val clear : t -> unit
+      val of_buffer : Buffer.t -> t
+    end
+    module Token : sig
+      type t
+      val lparen : t
+      val rparen : t
+      val lambda : t
+      val biglam : t
+      val pi : t
+      val colon : t
+      val hole : t
+      val sc : t
+      val at : t
+      val integer : string -> t
+      val ident : string -> t
+      val eof : t
+      val simple_string : string -> t
+      val hash_semi : t
+      val quoted_string : Lexing.position -> Quoted_string_buffer.t -> t
+      type s = Quoted_string_buffer.t -> Lexing.lexbuf -> t
+      val comment : string -> main:s -> s
+      val block_comment : Lexing.position -> main:s -> s
+    end
+  end
+
+
+  (* Create and populate a hashtable *)
+  let mk_hashtbl init =
+    let tbl = List.length init |> Hashtbl.create in
+    init |> List.iter (fun (k, v) -> Hashtbl.add tbl k v) ;
+    tbl
+
+  let keywords = mk_hashtbl [
+    ("check", CHECK);
+    ("define", DEFINE);
+    ("declare", DECLARE);
+    ("type", TYPE);
+    ("kind", KIND);
+    ("mpz", MPZ);
+    ("mpq", MPQ);
+    ("program", PROGRAM);
+    ("unsat", UNSAT);
+    ("sat", SAT);
+  ]
+
+  module Make (X : T) : sig
+    val main : ?buf:Buffer.t -> Lexing.lexbuf -> X.Token.t
+  end = struct (* BEGIN FUNCTOR BODY CONTAINING GENERATED CODE *)
+    open X
+
+}
+
+let lf = '\010'
+let lf_cr = ['\010' '\013']
+let dos_newline = "\013\010"
+let blank = [' ' '\009' '\012']
+let unquoted = [^ ';' '(' ')' '"' '\\' ':' '@' '!' ] # blank # lf_cr
+let digit = ['0'-'9']
+let hexdigit = digit | ['a'-'f' 'A'-'F']
+
+let unquoted_start =
+  unquoted # ['#' '|'] | '#' unquoted # ['|'] | '|' unquoted # ['#']
+
+let integer = digit+
+let ident = ('_')* ['a'-'z' 'A'-'Z' '\'' ]['a'-'z' 'A'-'Z' '0'-'9' '\\' '_']*
+
+
+rule main buf = parse
+  | lf | dos_newline { found_newline lexbuf 0;
+                       main buf lexbuf }
+  | blank+ { main buf lexbuf }
+  | (';' (_ # lf_cr)*) as text { Token.comment text ~main buf lexbuf }
+  | '(' { Token.lparen }
+  | ')' { Token.rparen }
+  | '\\' { Token.lambda }
+  | '!' { Token.pi }
+  | '%' { Token.biglam }
+  | '_' { Token.hole }
+  | ':' { Token.colon }
+  | '^' { Token.sc }
+  | '@' { Token.at }
+  | '(' '~' (integer as i) ')' {Token.integer ("-"^i) }
+  | integer as i { Token.integer i }
+  | '"'
+      { 
+        let pos = Lexing.lexeme_start_p lexbuf in
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf pos lexbuf;
+        let tok = Token.quoted_string pos buf in
+        Quoted_string_buffer.clear buf;
+        tok
+      }
+  | "#;" { Token.hash_semi }
+  | "#|"
+      {
+        let pos = Lexing.lexeme_start_p lexbuf in
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_block_comment buf [pos] lexbuf;
+        let tok = Token.block_comment pos ~main buf lexbuf in
+        Quoted_string_buffer.clear buf;
+        tok
+      }
+  | "|#" { main_failure lexbuf "illegal end of comment" }
+  | "#" "#"+ "|" unquoted* (* unquoted_start can match ##, so ##| (which should be
+                              refused) would not not be parsed by this case if the regexp
+                              on the left was not there *)
+  | "|" "|"+ "#" unquoted*
+  | unquoted_start unquoted* ("#|" | "|#") unquoted*
+      { main_failure lexbuf "comment tokens in unquoted atom" }
+  | "#" | "|" | unquoted_start unquoted* as str { Token.simple_string str }
+  | eof { Token.eof }
+
+and scan_string buf start = parse
+  | '"' { Quoted_string_buffer.add_lexeme buf lexbuf; () }
+  | '\\' lf [' ' '\t']*
+      {
+        let len = lexeme_len lexbuf - 2 in
+        found_newline lexbuf len;
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | '\\' dos_newline [' ' '\t']*
+      {
+        let len = lexeme_len lexbuf - 3 in
+        found_newline lexbuf len;
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c)
+      {
+        Quoted_string_buffer.add_char buf (char_for_backslash c);
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | '\\' (digit as c1) (digit as c2) (digit as c3)
+      {
+        let v = dec_code c1 c2 c3 in
+        if v > 255 then (
+          let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_end_p lexbuf in
+          let msg =
+            sprintf
+              "Sexplib.Lexer.scan_string: \
+               illegal escape at line %d char %d: `\\%c%c%c'"
+              pos_lnum (pos_cnum - pos_bol - 3)
+              c1 c2 c3 in
+          failwith msg);
+        Quoted_string_buffer.add_char buf (Char.chr v);
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
+      {
+        let v = hex_code c1 c2 in
+        Quoted_string_buffer.add_char buf (Char.chr v);
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | '\\' (_ as c)
+      {
+        Quoted_string_buffer.add_char buf '\\';
+        Quoted_string_buffer.add_char buf c;
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | lf
+      {
+        found_newline lexbuf 0;
+        Quoted_string_buffer.add_char buf lf;
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | ([^ '\\' '"'] # lf)+
+      {
+        let ofs = lexbuf.lex_start_pos in
+        let len = lexbuf.lex_curr_pos - ofs in
+        Quoted_string_buffer.add_substring buf lexbuf.lex_buffer ofs len;
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_string buf start lexbuf
+      }
+  | eof
+      {
+        let msg =
+          sprintf
+            "Sexplib.Lexer.scan_string: unterminated string at line %d char %d"
+            start.pos_lnum (start.pos_cnum - start.pos_bol)
+        in
+        failwith msg
+      }
+
+and scan_block_comment buf locs = parse
+  | ('#'* | '|'*) lf
+      { Quoted_string_buffer.add_lexeme buf lexbuf;
+        found_newline lexbuf 0; scan_block_comment buf locs lexbuf }
+  | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+
+      { Quoted_string_buffer.add_lexeme buf lexbuf;
+        scan_block_comment buf locs lexbuf }
+  | ('#'* | '|'*) '"'
+      {
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        let cur = lexeme_end_p lexbuf in
+        let start = { cur with pos_cnum = cur.pos_cnum - 1 } in
+        scan_string buf start lexbuf;
+        scan_block_comment buf locs lexbuf
+      }
+  | '#'+ '|'
+    {
+      Quoted_string_buffer.add_lexeme buf lexbuf;
+      let cur = lexeme_end_p lexbuf in
+      let start = { cur with pos_cnum = cur.pos_cnum - 2 } in
+      scan_block_comment buf (start :: locs) lexbuf
+    }
+  | '|'+ '#'
+      {
+        Quoted_string_buffer.add_lexeme buf lexbuf;
+        match locs with
+        | [_] -> () (* the comment is finished *)
+        | _ :: (_ :: _ as t) -> scan_block_comment buf t lexbuf
+        | [] -> assert false  (* impossible *)
+      }
+  | eof
+      {
+        match locs with
+        | [] -> assert false
+        | { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } :: _ ->
+            let msg =
+              sprintf "Sexplib.Lexer.scan_block_comment: \
+                unterminated block comment at line %d char %d"
+                pos_lnum (pos_cnum - pos_bol)
+            in
+            failwith msg
+      }
+
+{ (* RESUME FUNCTOR BODY CONTAINING GENERATED CODE *)
+
+    let main ?buf =
+      let buf =
+        match buf with
+        | None -> Quoted_string_buffer.create 64
+        | Some buf ->
+          Buffer.clear buf;
+          Quoted_string_buffer.of_buffer buf
+      in
+      main buf
+
+  end (* END FUNCTOR BODY CONTAINING GENERATED CODE *)
+
+  module Vanilla =
+    Make (struct
+      module Quoted_string_buffer = struct
+        include Buffer
+        let add_lexeme _ _ = ()
+        let of_buffer b = b
+      end
+      module Token = struct
+        open LfscParser
+        type t = token
+        type s = Quoted_string_buffer.t -> Lexing.lexbuf -> t
+        let eof = EOF
+        let lparen = LPAREN
+        let rparen = RPAREN
+        let lambda = LAMBDA
+        let pi = PI
+        let biglam =  BIGLAMBDA
+        let hole = HOLE
+        let colon = COLON
+        let sc = SC
+        let at = AT
+        let hash_semi = HASH_SEMI
+        let integer i = INT (Big_int.big_int_of_string i)
+        let ident i =
+          try Hashtbl.find keywords i with Not_found -> STRING i
+        let simple_string x =
+          try Hashtbl.find keywords x with Not_found -> STRING x
+        let quoted_string _ buf = STRING (Buffer.contents buf)
+        let block_comment _pos ~main buf lexbuf =
+          main buf lexbuf
+        let comment _text ~main buf lexbuf =
+          main buf lexbuf (* skip and continue lexing *)
+      end
+    end)
+
+
+  let main = Vanilla.main
+
+}