From 7021c53d4ecf97c82ccebb6bb45f5305d8b482ea Mon Sep 17 00:00:00 2001 From: ckeller Date: Mon, 28 Jan 2019 23:19:12 +0100 Subject: 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 --- src/trace/smtAtom.ml | 1143 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 931 insertions(+), 212 deletions(-) (limited to 'src/trace/smtAtom.ml') diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 7ccaa95..6554a8f 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1,13 +1,9 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) @@ -16,30 +12,58 @@ open SmtMisc open CoqTerms +open Entries +open Declare +open Decl_kinds open SmtBtype + (** Operators *) type cop = - | CO_xH - | CO_Z0 + | CO_xH + | CO_Z0 + | CO_BV of bool list type uop = - | UO_xO - | UO_xI - | UO_Zpos - | UO_Zneg - | UO_Zopp + | UO_xO + | UO_xI + | UO_Zpos + | UO_Zneg + | UO_Zopp + | UO_BVbitOf of int * int + | UO_BVnot of int + | UO_BVneg of int + | UO_BVextr of int * int * int + | UO_BVzextn of int * int + | UO_BVsextn of int * int type bop = - | BO_Zplus - | BO_Zminus - | BO_Zmult - | BO_Zlt - | BO_Zle - | BO_Zge - | BO_Zgt - | BO_eq of btype + | BO_Zplus + | BO_Zminus + | BO_Zmult + | BO_Zlt + | BO_Zle + | BO_Zge + | BO_Zgt + | BO_eq of btype + | BO_BVand of int + | BO_BVor of int + | BO_BVxor of int + | BO_BVadd of int + | BO_BVmult of int + | BO_BVult of int + | BO_BVslt of int + | BO_BVconcat of int * int + | BO_BVshl of int + | BO_BVshr of int + | BO_select of btype * btype + | BO_diffarray of btype * btype + + +type top = + | TO_store of btype * btype + type nop = | NO_distinct of btype @@ -55,26 +79,35 @@ type index = Index of int type indexed_op = index * op_def let destruct s (i, hval) = match i with - | Index index -> index, hval - | Rel_name _ -> failwith s + | Index index -> index, hval + | Rel_name _ -> failwith s + +let dummy_indexed_op i dom codom = + (i, {tparams = dom; tres = codom; op_val = Term.mkProp}) + +let indexed_op_index i = + let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in + index -let dummy_indexed_op i dom codom = i, {tparams = dom; tres = codom; op_val = Term.mkProp} -let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in - index +let debruijn_indexed_op i ty = + (Index i, {tparams = [||]; tres = ty; op_val = Term.mkRel i}) module Op = struct let c_to_coq = function | CO_xH -> Lazy.force cCO_xH | CO_Z0 -> Lazy.force cCO_Z0 + | CO_BV bv -> mklApp cCO_BV [|mk_bv_list bv; mkN (List.length bv)|] let c_type_of = function | CO_xH -> Tpositive | CO_Z0 -> TZ + | CO_BV bv -> TBV (List.length bv) let interp_cop = function | CO_xH -> Lazy.force cxH | CO_Z0 -> Lazy.force cZ0 + | CO_BV bv -> mklApp cof_bits [|mk_bv_list bv|] let u_to_coq = function | UO_xO -> Lazy.force cUO_xO @@ -82,14 +115,29 @@ module Op = | UO_Zpos -> Lazy.force cUO_Zpos | UO_Zneg -> Lazy.force cUO_Zneg | UO_Zopp -> Lazy.force cUO_Zopp + | UO_BVbitOf (s, i) -> mklApp cUO_BVbitOf [|mkN s; mkNat i|] + | UO_BVnot s -> mklApp cUO_BVnot [|mkN s|] + | UO_BVneg s -> mklApp cUO_BVneg [|mkN s|] + | UO_BVextr (i, n, s) -> mklApp cUO_BVextr [|mkN i; mkN n; mkN s|] + | UO_BVzextn (s, n) -> mklApp cUO_BVzextn [|mkN s; mkN n|] + | UO_BVsextn (s, n) -> mklApp cUO_BVsextn [|mkN s; mkN n|] let u_type_of = function | UO_xO | UO_xI -> Tpositive | UO_Zpos | UO_Zneg | UO_Zopp -> TZ + | UO_BVbitOf _ -> Tbool + | UO_BVnot s | UO_BVneg s -> TBV s + | UO_BVextr (_, n, _) -> TBV n + | UO_BVzextn (s, n) | UO_BVsextn (s, n) -> TBV (s + n) let u_type_arg = function | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive | UO_Zopp -> TZ + | UO_BVbitOf (s,_) -> TBV s + | UO_BVnot s | UO_BVneg s -> TBV s + | UO_BVextr (_, _, s) -> TBV s + | UO_BVzextn (s, _) | UO_BVsextn (s, _) -> TBV s + let interp_uop = function | UO_xO -> Lazy.force cxO @@ -97,8 +145,17 @@ module Op = | UO_Zpos -> Lazy.force cZpos | UO_Zneg -> Lazy.force cZneg | UO_Zopp -> Lazy.force copp + | UO_BVbitOf (s,i) -> mklApp cbitOf [|mkN s; mkNat i|] + | UO_BVnot s -> mklApp cbv_not [|mkN s|] + | UO_BVneg s -> mklApp cbv_neg [|mkN s|] + | UO_BVextr (i, n, s) -> mklApp cbv_extr [|mkN i; mkN n; mkN s|] + | UO_BVzextn (s, n) -> mklApp cbv_zextn [|mkN s; mkN n|] + | UO_BVsextn (s, n) -> mklApp cbv_sextn [|mkN s; mkN n|] let eq_tbl = Hashtbl.create 17 + let select_tbl = Hashtbl.create 17 + let store_tbl = Hashtbl.create 17 + let diffarray_tbl = Hashtbl.create 17 let eq_to_coq t = try Hashtbl.find eq_tbl t @@ -107,6 +164,27 @@ module Op = Hashtbl.add eq_tbl t op; op + let select_to_coq ti te = + try Hashtbl.find select_tbl (ti, te) + with Not_found -> + let op = mklApp cBO_select [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in + Hashtbl.add select_tbl (ti, te) op; + op + + let store_to_coq ti te = + try Hashtbl.find store_tbl (ti, te) + with Not_found -> + let op = mklApp cTO_store [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in + Hashtbl.add store_tbl (ti, te) op; + op + + let diffarray_to_coq ti te = + try Hashtbl.find diffarray_tbl (ti, te) + with Not_found -> + let op = mklApp cBO_diffarray [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in + Hashtbl.add diffarray_tbl (ti, te) op; + op + let b_to_coq = function | BO_Zplus -> Lazy.force cBO_Zplus | BO_Zminus -> Lazy.force cBO_Zminus @@ -116,23 +194,97 @@ module Op = | BO_Zge -> Lazy.force cBO_Zge | BO_Zgt -> Lazy.force cBO_Zgt | BO_eq t -> eq_to_coq t + | BO_BVand s -> mklApp cBO_BVand [|mkN s|] + | BO_BVor s -> mklApp cBO_BVor [|mkN s|] + | BO_BVxor s -> mklApp cBO_BVxor [|mkN s|] + | BO_BVadd s -> mklApp cBO_BVadd [|mkN s|] + | BO_BVmult s -> mklApp cBO_BVmult [|mkN s|] + | BO_BVult s -> mklApp cBO_BVult [|mkN s|] + | BO_BVslt s -> mklApp cBO_BVslt [|mkN s|] + | BO_BVconcat (s1, s2) -> mklApp cBO_BVconcat [|mkN s1; mkN s2|] + | BO_BVshl s -> mklApp cBO_BVshl [|mkN s|] + | BO_BVshr s -> mklApp cBO_BVshr [|mkN s|] + | BO_select (ti, te) -> select_to_coq ti te + | BO_diffarray (ti, te) -> diffarray_to_coq ti te let b_type_of = function | BO_Zplus | BO_Zminus | BO_Zmult -> TZ - | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _ -> Tbool + | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _ + | BO_BVult _ | BO_BVslt _ -> Tbool + | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s + | BO_BVshl s | BO_BVshr s -> TBV s + | BO_BVconcat (s1, s2) -> TBV (s1 + s2) + | BO_select (_, te) -> te + | BO_diffarray (ti, _) -> ti let b_type_args = function - | BO_Zplus | BO_Zminus | BO_Zmult + | BO_Zplus | BO_Zminus | BO_Zmult | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (TZ,TZ) | BO_eq t -> (t,t) - - let interp_eq = function + | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s + | BO_BVult s | BO_BVslt s | BO_BVshl s | BO_BVshr s -> + (TBV s,TBV s) + | BO_BVconcat (s1, s2) -> (TBV s1, TBV s2) + | BO_select (ti, te) -> (TFArray (ti, te), ti) + | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te)) + + + let interp_ieq t_i t = + mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] + + (* let veval_t te = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, ty = Typing.type_of env evd te in + Vnorm.cbv_vm env te ty + + + let interp_ieq_eval t_i t = + let te = mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] in + veval_t te + *) + + let interp_eqarray t_i ti te = + mklApp cequalarray + SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i te |] + + let interp_select t_i ti te = + mklApp cselect + SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.inh_interp t_i te|] + + let interp_diff t_i ti te = + mklApp cdiff + SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |] + + + let interp_store t_i ti te = + mklApp cstore + SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |] + + + let interp_eq t_i = function | TZ -> Lazy.force ceqbZ | Tbool -> Lazy.force ceqb | Tpositive -> Lazy.force ceqbP - | Tindex i -> mklApp cte_eqb [|indexed_type_hval i|] + | TBV s -> mklApp cbv_eq [|mkN s|] + | Tindex i -> + mklApp ceqb_of_compdec [|mklApp cte_carrier [|i.hval|]; + mklApp cte_compdec [|i.hval|]|] + | TFArray (ti, te) -> interp_eqarray t_i ti te + + - let interp_bop = function + let interp_bop t_i = function | BO_Zplus -> Lazy.force cadd | BO_Zminus -> Lazy.force csub | BO_Zmult -> Lazy.force cmul @@ -140,7 +292,32 @@ module Op = | BO_Zle -> Lazy.force cleb | BO_Zge -> Lazy.force cgeb | BO_Zgt -> Lazy.force cgtb - | BO_eq t -> interp_eq t + | BO_eq t -> interp_eq t_i t + | BO_BVand s -> mklApp cbv_and [|mkN s|] + | BO_BVor s -> mklApp cbv_or [|mkN s|] + | BO_BVxor s -> mklApp cbv_xor [|mkN s|] + | BO_BVadd s -> mklApp cbv_add [|mkN s|] + | BO_BVmult s -> mklApp cbv_mult [|mkN s|] + | BO_BVult s -> mklApp cbv_ult [|mkN s|] + | BO_BVslt s -> mklApp cbv_slt [|mkN s|] + | BO_BVconcat (s1,s2) -> mklApp cbv_concat [|mkN s1; mkN s2|] + | BO_BVshl s -> mklApp cbv_shl [|mkN s|] + | BO_BVshr s -> mklApp cbv_shr [|mkN s|] + | BO_select (ti, te) -> interp_select t_i ti te + | BO_diffarray (ti, te) -> interp_diff t_i ti te + + let t_to_coq = function + | TO_store (ti, te) -> store_to_coq ti te + + let t_type_of = function + | TO_store (ti, te) -> TFArray (ti, te) + + let t_type_args = function + | TO_store (ti, te) -> TFArray (ti, te), ti, te + + let interp_top t_i = function + | TO_store (ti, te) -> interp_store t_i ti te + let n_to_coq = function | NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|] @@ -151,14 +328,9 @@ module Op = let n_type_args = function | NO_distinct ty -> ty - let interp_distinct = function - | TZ -> Lazy.force cZ - | Tbool -> Lazy.force cbool - | Tpositive -> Lazy.force cpositive - | Tindex i -> mklApp cte_carrier [|indexed_type_hval i|] - - let interp_nop = function - | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|] + let interp_nop t_i = function + | NO_distinct ty -> + mklApp cdistinct [|SmtBtype.interp t_i ty; interp_eq t_i ty|] let i_to_coq i = let index, _ = destruct "destruct on a Rel: called by i_to_coq" i in mkInt index @@ -206,14 +378,50 @@ module Op = (index, hval.tparams, hval.tres, op)::acc in Hashtbl.fold set reify.tbl [] - let c_equal op1 op2 = op1 == op2 + let c_equal op1 op2 = match op1, op2 with + | CO_BV bv1, CO_BV bv2 -> + (try List.for_all2 (=) bv1 bv2 with + | Invalid_argument _ -> false) + | _ -> op1 == op2 - let u_equal op1 op2 = op1 == op2 + let u_equal op1 op2 = + match op1,op2 with + | UO_xO, UO_xO + | UO_xI, UO_xI + | UO_Zpos, UO_Zpos + | UO_Zneg, UO_Zneg + | UO_Zopp, UO_Zopp -> true + | UO_BVbitOf (s1,i1), UO_BVbitOf (s2,i2) -> s1 == s2 && i1 == i2 + | UO_BVnot s1, UO_BVnot s2 -> s1 == s2 + | UO_BVneg s1, UO_BVneg s2 -> s1 == s2 + | UO_BVextr (i1, n1, s1) , UO_BVextr (i2, n2, s2) -> + i1 == i2 && n1 == n2 && s1 == s2 + | UO_BVzextn (s1, n1), UO_BVzextn (s2, n2) -> s1 == s2 && n1 == n2 + | UO_BVsextn (s1, n1), UO_BVsextn (s2, n2) -> s1 == s2 && n1 == n2 + | _ -> false let b_equal op1 op2 = match op1,op2 with - | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2 - | _ -> op1 == op2 + | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2 + | BO_BVand n1, BO_BVand n2 -> n1 == n2 + | BO_BVor n1, BO_BVor n2 -> n1 == n2 + | BO_BVxor n1, BO_BVxor n2 -> n1 == n2 + | BO_BVadd n1, BO_BVadd n2 -> n1 == n2 + | BO_BVmult n1, BO_BVmult n2 -> n1 == n2 + | BO_BVult n1, BO_BVult n2 -> n1 == n2 + | BO_BVslt n1, BO_BVslt n2 -> n1 == n2 + | BO_BVconcat (n1,m1), BO_BVconcat (n2,m2) -> n1 == n2 && m1 == m2 + | BO_BVshl n1, BO_BVshl n2 -> n1 == n2 + | BO_BVshr n1, BO_BVshr n2 -> n1 == n2 + | BO_select (ti1, te1), BO_select (ti2, te2) + | BO_diffarray (ti1, te1), BO_diffarray (ti2, te2) -> + SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2 + | _ -> op1 == op2 + + let t_equal op1 op2 = + match op1,op2 with + | TO_store (ti1, te1), TO_store (ti2, te2) -> + SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2 let n_equal op1 op2 = match op1,op2 with @@ -221,6 +429,62 @@ module Op = let i_equal (i1, _) (i2, _) = i1 = i2 + + + + let logic_of_cop = function + | CO_xH | CO_Z0 -> SL.singleton LLia + | CO_BV _ -> SL.singleton LBitvectors + + let logic_of_uop = function + | UO_xO | UO_xI + | UO_Zpos | UO_Zneg | UO_Zopp -> SL.singleton LLia + | UO_BVbitOf _ | UO_BVnot _ | UO_BVneg _ + | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> SL.singleton LBitvectors + + let logic_of_bop = function + | BO_Zplus + | BO_Zminus + | BO_Zmult + | BO_Zlt + | BO_Zle + | BO_Zge + | BO_Zgt -> SL.singleton LLia + | BO_eq ty -> SmtBtype.logic ty + | BO_BVand _ + | BO_BVor _ + | BO_BVxor _ + | BO_BVadd _ + | BO_BVmult _ + | BO_BVult _ + | BO_BVslt _ + | BO_BVshl _ + | BO_BVshr _ + | BO_BVconcat _ -> SL.singleton LBitvectors + | BO_select (ti, te) + | BO_diffarray (ti, te) -> + SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te)) + + + let logic_of_top = function + | TO_store (ti, te) -> + SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te)) + + let logic_of_nop = function + | NO_distinct ty -> SmtBtype.logic ty + + + let logic_of_indexed t = + let (_, hval) = destruct "destruct on a Rel: called by logic_of_indexed" t in + Array.fold_left (fun l ty -> + SL.union (SmtBtype.logic ty) l + ) (SmtBtype.logic hval.tres) hval.tparams + + + let logic_ro reify = + Hashtbl.fold (fun _ op -> SL.union (logic_of_indexed op)) + reify.tbl SL.empty + end @@ -230,6 +494,7 @@ type atom = | Acop of cop | Auop of uop * hatom | Abop of bop * hatom * hatom + | Atop of top * hatom * hatom * hatom | Anop of nop * hatom array | Aapp of indexed_op * hatom array @@ -271,17 +536,24 @@ module HashedAtom = | Acop opa, Acop opb -> Op.c_equal opa opb | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) -> - Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index + Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index + | Atop(opa,ha1,ha2,ha3), Atop(opb,hb1,hb2,hb3) -> + Op.t_equal opa opb && ha1.index == hb1.index && + ha2.index == hb2.index && ha3.index == hb3.index | Anop (opa,ha), Anop (opb,hb) -> - let na = Array.length ha in - let nb = Array.length hb in - let i = ref (-1) in - Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.n_equal opa opb && na == nb && + Array.fold_left + (fun b h -> incr i; b && h.index == hb.(!i).index) true ha | Aapp (va,ha), Aapp (vb,hb) -> - let na = Array.length ha in - let nb = Array.length hb in - let i = ref (-1) in - Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.i_equal va vb && na == nb && + Array.fold_left + (fun b h -> incr i; b && h.index == hb.(!i).index) true ha | _, _ -> false let hash = function @@ -289,24 +561,31 @@ module HashedAtom = | Auop (op,h) -> (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2 | Abop (op,h1,h2) -> - (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3 + (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3 + | Atop (op,h1,h2,h3) -> + (((( ((h1.index lsl 2) + h2.index) lsl 3) + h3.index) lsl 4 + + Hashtbl.hash op) lsl 4) lxor 4 | Anop (op, args) -> - let hash_args = - match Array.length args with - | 0 -> 0 - | 1 -> args.(0).index - | 2 -> args.(1).index lsl 2 + args.(0).index - | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in - (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4 + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index + in + (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4 | Aapp (op, args) -> let op_index = try fst (destruct "destruct on a Rel: called by hash" op) with _ -> 0 in - let hash_args = - match Array.length args with - | 0 -> 0 - | 1 -> args.(0).index - | 2 -> args.(1).index lsl 2 + args.(0).index - | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in - (hash_args lsl 5 + op_index lsl 3) lxor 4 + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index + in + (hash_args lsl 5 + op_index lsl 3) lxor 4 + + end @@ -327,124 +606,189 @@ module Atom = | Acop op -> Op.c_type_of op | Auop (op,_) -> Op.u_type_of op | Abop (op,_,_) -> Op.b_type_of op + | Atop (op,_,_,_) -> Op.t_type_of op | Anop (op,_) -> Op.n_type_of op | Aapp (op,_) -> Op.i_type_of op let is_bool_type h = SmtBtype.equal (type_of h) Tbool + let is_bv_type h = match type_of h with | TBV _ -> true | _ -> false let rec compute_int = function | Acop c -> (match c with | CO_xH -> 1 - | CO_Z0 -> 0) + | CO_Z0 -> 0 + | CO_BV _ -> assert false) | Auop (op,h) -> (match op with | UO_xO -> 2*(compute_hint h) | UO_xI -> 2*(compute_hint h) + 1 | UO_Zpos -> compute_hint h | UO_Zneg -> - (compute_hint h) - | UO_Zopp -> assert false) + | UO_Zopp | UO_BVbitOf _ + | UO_BVnot _ | UO_BVneg _ + | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> assert false) | _ -> assert false and compute_hint h = compute_int (atom h) - let to_string_int i = + let to_smt_int fmt i = let s1 = if i < 0 then "(- " else "" in let s2 = if i < 0 then ")" else "" in let j = if i < 0 then -i else i in - s1 ^ string_of_int j ^ s2 - - let to_string ?pi:(pi=false) h = - let rec to_string h = - (if pi then string_of_int (index h) ^":" else "") - ^ to_string_atom (atom h) - - and to_string_atom = function - | Acop _ as a -> to_string_int (compute_int a) - | Auop (UO_Zopp,h) -> - "(- " ^ - to_string h ^ - ")" - | Auop _ as a -> to_string_int (compute_int a) - | Abop (op,h1,h2) -> to_string_bop op h1 h2 - | Anop (op,a) -> to_string_nop op a - | Aapp ((i, op), a) -> - let op_string = begin match i with - | Index index -> "op_" ^ string_of_int index - | Rel_name name -> name end - ^ if pi then to_string_op op else "" in + Format.fprintf fmt "%s%i%s" s1 j s2 + + + let rec bv_to_smt fmt = function + | true :: bv -> Format.fprintf fmt "%a1" bv_to_smt bv + | false :: bv -> Format.fprintf fmt "%a0" bv_to_smt bv + | [] -> () + + + let to_smt_named ?pi:(pi=false) (fmt:Format.formatter) h = + let rec to_smt fmt h = + if pi then Format.fprintf fmt "%d:" (index h); + to_smt_atom (atom h) + + and to_smt_atom = function + | Acop (CO_BV bv) -> Format.fprintf fmt "#b%a" bv_to_smt bv + | Acop _ as a -> to_smt_int fmt (compute_int a) + | Auop (UO_Zopp,h) -> + Format.fprintf fmt "(- "; + to_smt fmt h; + Format.fprintf fmt ")" + | Auop (UO_BVbitOf (_, i), h) -> + Format.fprintf fmt "(bitof %d %a)" i to_smt h + | Auop (UO_BVnot _, h) -> + Format.fprintf fmt "(bvnot %a)" to_smt h + | Auop (UO_BVneg _, h) -> + Format.fprintf fmt "(bvneg %a)" to_smt h + | Auop (UO_BVextr (i, n, _), h) -> + Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h + | Auop (UO_BVzextn (_, n), h) -> + Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h + | Auop (UO_BVsextn (_, n), h) -> + Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h + | Auop _ as a -> to_smt_int fmt (compute_int a) + | Abop (op,h1,h2) -> to_smt_bop op h1 h2 + | Atop (op,h1,h2,h3) -> to_smt_top op h1 h2 h3 + | Anop (op,a) -> to_smt_nop op a + | Aapp ((i,op),a) -> + let op_smt () = + (match i with + | Index index -> Format.fprintf fmt "op_%i" index + | Rel_name name -> Format.fprintf fmt "%s" name); + if pi then to_smt_op op + in if Array.length a = 0 then ( - op_string + op_smt () ) else ( - "(" ^ op_string ^ - Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^ - ")" + Format.fprintf fmt "("; + op_smt (); + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" ) - and to_string_op {tparams=bta; tres=bt; op_val=t} = - "[(" ^ Array.fold_left (fun acc bt -> acc ^ SmtBtype.to_string bt ^ " ") - " " bta ^ ") ( " ^ SmtBtype.to_string bt ^ " ) ( " ^ - Pp.string_of_ppcmds (Printer.pr_constr t) ^ " )]" - and to_string_bop op h1 h2 = + and to_smt_op {tparams=bta; tres=bt; op_val=t} = + Format.fprintf fmt "[("; + Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta; + Format.fprintf fmt ") ( "; + SmtBtype.to_smt fmt bt; + Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Printer.pr_constr t)) + + and to_smt_bop op h1 h2 = let s = match op with - | BO_Zplus -> "+" - | BO_Zminus -> "-" - | BO_Zmult -> "*" - | BO_Zlt -> "<" - | BO_Zle -> "<=" - | BO_Zge -> ">=" - | BO_Zgt -> ">" - | BO_eq _ -> "=" in - "(" ^ s ^ " " ^ - to_string h1 ^ - " " ^ - to_string h2 ^ - ")" - - and to_string_nop op a = + | BO_Zplus -> "+" + | BO_Zminus -> "-" + | BO_Zmult -> "*" + | BO_Zlt -> "<" + | BO_Zle -> "<=" + | BO_Zge -> ">=" + | BO_Zgt -> ">" + | BO_eq _ -> "=" + | BO_BVand _ -> "bvand" + | BO_BVor _ -> "bvor" + | BO_BVxor _ -> "bvxor" + | BO_BVadd _ -> "bvadd" + | BO_BVmult _ -> "bvmul" + | BO_BVult _ -> "bvult" + | BO_BVslt _ -> "bvslt" + | BO_BVconcat _ -> "concat" + | BO_BVshl _ -> "bvshl" + | BO_BVshr _ -> "bvlshr" + | BO_select _ -> "select" + | BO_diffarray _ -> "diff" (* should not be used in goals *) + in + Format.fprintf fmt "(%s %a %a)" s to_smt h1 to_smt h2 + + and to_smt_top op h1 h2 h3= let s = match op with - | NO_distinct _ -> "distinct" in - "(" ^ s ^ - Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^ - ")" in - to_string h + | TO_store _ -> "store" + in + Format.fprintf fmt "(%s %a %a %a)" s to_smt h1 to_smt h2 to_smt h3 + + and to_smt_nop op a = + let s = match op with + | NO_distinct _ -> "distinct" in + Format.fprintf fmt "(%s" s; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" + + in + to_smt fmt h - let to_smt fmt t = Format.fprintf fmt "%s@." (to_string t) + let to_smt (fmt:Format.formatter) h = to_smt_named fmt h exception NotWellTyped of atom let check a = + (* Format.eprintf "Checking %a @." to_smt_atom a; *) match a with | Acop _ -> () | Auop(op,h) -> - if not (SmtBtype.equal (Op.u_type_arg op) (type_of h)) - then raise (NotWellTyped a) + if not (SmtBtype.equal (Op.u_type_arg op) (type_of h)) then + raise (NotWellTyped a) | Abop(op,h1,h2) -> - let (t1,t2) = Op.b_type_args op in - if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2)) - then raise (NotWellTyped a) + let (t1,t2) = Op.b_type_args op in + if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2)) + then (Format.eprintf "1. Wanted %a, got %a@.2. Wanted %a, got %a@." + SmtBtype.to_smt t1 SmtBtype.to_smt (type_of h1) + SmtBtype.to_smt t2 SmtBtype.to_smt (type_of h2); + raise (NotWellTyped a)) + | Atop(op,h1,h2,h3) -> + let (t1,t2,t3) = Op.t_type_args op in + if not (SmtBtype.equal t1 (type_of h1) && + SmtBtype.equal t2 (type_of h2) && + SmtBtype.equal t3 (type_of h3)) + then raise (NotWellTyped a) | Anop(op,ha) -> - let ty = Op.n_type_args op in - Array.iter (fun h -> if not (SmtBtype.equal ty (type_of h)) then raise (NotWellTyped a)) ha + let ty = Op.n_type_args op in + Array.iter + (fun h -> if not (SmtBtype.equal ty (type_of h)) then + raise (NotWellTyped a)) ha | Aapp(op,args) -> - let tparams = Op.i_type_args op in - Array.iteri (fun i t -> - if not (SmtBtype.equal t (type_of args.(i))) then - raise (NotWellTyped a)) tparams + let tparams = Op.i_type_args op in + Array.iteri (fun i t -> + if not (SmtBtype.equal t (type_of args.(i))) then + (Format.eprintf "Wanted %a, got %a@." + SmtBtype.to_smt t SmtBtype.to_smt (type_of args.(i)); + raise (NotWellTyped a))) tparams type reify_tbl = { mutable count : int; - tbl : hatom HashAtom.t + tbl : hatom HashAtom.t } - let create () = { count = 0; tbl = HashAtom.create 17 } + let op_coq_terms = Hashtbl.create 17 + let clear reify = + Hashtbl.clear op_coq_terms; reify.count <- 0; HashAtom.clear reify.tbl @@ -461,7 +805,7 @@ module Atom = with Not_found -> declare reify a else {index = -1; hval = a} - let mk_eq reify decl ty h1 h2 = + let mk_eq reify ?declare:(decl=true) ty h1 h2 = let op = BO_eq ty in try HashAtom.find reify.tbl (Abop (op, h1, h2)) @@ -473,7 +817,7 @@ module Atom = let mk_neg reify ({index = i; hval = a} as ha) = try HashAtom.find reify.tbl (Auop (UO_Zopp, ha)) - with Not_found -> + with Not_found -> let na = match a with | Auop (UO_Zpos, x) -> Auop (UO_Zneg, x) | Auop (UO_Zneg, x) -> Auop (UO_Zpos, x) @@ -481,20 +825,25 @@ module Atom = get reify na let rec hash_hatom ra' {index = _; hval = a} = - match a with + match a with | Acop cop -> get ra' a | Auop (uop, ha) -> get ra' (Auop (uop, hash_hatom ra' ha)) | Abop (bop, ha1, ha2) -> let new_ha1 = hash_hatom ra' ha1 in let new_ha2 = hash_hatom ra' ha2 in begin match bop with - | BO_eq ty -> mk_eq ra' true ty new_ha1 new_ha2 + | BO_eq ty -> mk_eq ra' ~declare:true ty new_ha1 new_ha2 | _ -> get ra' (Abop (bop, new_ha1, new_ha2)) end + | Atop (top, ha1, ha2, ha3) -> + let new_ha1 = hash_hatom ra' ha1 in + let new_ha2 = hash_hatom ra' ha2 in + let new_ha3 = hash_hatom ra' ha3 in + get ra' (Atop (top, new_ha1, new_ha2, new_ha3)) | Anop _ -> assert false | Aapp (op, arr) -> get ra' (Aapp (op, Array.map (hash_hatom ra') arr)) - + let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t} - + let print_atoms reify where = let oc = open_out where in let fmt = Format.formatter_of_out_channel oc in @@ -513,11 +862,15 @@ module Atom = type coq_cst = | CCxH | CCZ0 + | CCBV | CCxO | CCxI | CCZpos | CCZneg | CCZopp + | CCBVbitOf + | CCBVnot + | CCBVneg | CCZplus | CCZminus | CCZmult @@ -525,39 +878,164 @@ module Atom = | CCZle | CCZge | CCZgt + | CCBVand + | CCBVor + | CCBVxor + | CCBVadd + | CCBVmult + | CCBVult + | CCBVslt + | CCBVconcat + | CCBVextr + | CCBVsextn + | CCBVzextn + | CCBVshl + | CCBVshr | CCeqb | CCeqbP | CCeqbZ + | CCeqbBV + | CCeqbA + | CCselect + | CCdiff + | CCstore | CCunknown + | CCunknown_deps of int + + + let logic_coq_cst = function + | CCxH + | CCZ0 + | CCxO + | CCxI + | CCZpos + | CCZneg + | CCZopp + | CCZplus + | CCZminus + | CCZmult + | CCZlt + | CCZle + | CCZge + | CCZgt -> SL.singleton LLia + + | CCBV + | CCBVbitOf + | CCBVnot + | CCBVneg + | CCBVand + | CCBVor + | CCBVxor + | CCBVadd + | CCBVmult + | CCBVult + | CCBVslt + | CCBVconcat + | CCBVextr + | CCBVsextn + | CCBVzextn + | CCBVshl + | CCBVshr -> SL.singleton LBitvectors + + | CCselect | CCdiff | CCstore -> SL.singleton LArrays + + | CCeqb -> SL.empty + + (* | CCeqbP | CCeqbZ -> SL.singleton LLia *) + (* | CCeqbBV -> SL.singleton LBitvectors *) + (* | CCeqbA -> SL.singleton LArrays *) + + | CCeqbP | CCeqbZ | CCeqbBV | CCeqbA + | CCunknown | CCunknown_deps _ -> SL.singleton LUF + + + let gobble_of_coq_cst = function + | CCBV + | CCBVbitOf + | CCBVnot + | CCBVneg + | CCBVand + | CCBVor + | CCBVxor + | CCBVadd + | CCBVmult + | CCBVult + | CCBVslt + | CCBVsextn + | CCBVzextn + | CCBVshl + | CCBVshr -> 1 + + | CCBVconcat -> 2 + | CCBVextr -> 3 + + | CCselect -> 5 + | CCdiff -> 10 + | CCstore -> 8 + + | _ -> 0 + let op_tbl () = let tbl = Hashtbl.create 29 in let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in List.iter add - [ cxH,CCxH; cZ0,CCZ0; + [ cxH,CCxH; cZ0,CCZ0; cof_bits, CCBV; cxO,CCxO; cxI,CCxI; cZpos,CCZpos; cZneg,CCZneg; copp,CCZopp; + cbitOf, CCBVbitOf; cbv_not, CCBVnot; cbv_neg, CCBVneg; + cbv_extr, CCBVextr; cbv_zextn, CCBVzextn; cbv_sextn, CCBVsextn; cadd,CCZplus; csub,CCZminus; cmul,CCZmult; cltb,CCZlt; - cleb,CCZle; cgeb,CCZge; cgtb,CCZgt; ceqb,CCeqb; ceqbP,CCeqbP; - ceqbZ, CCeqbZ + cleb,CCZle; cgeb,CCZge; cgtb,CCZgt; + cbv_and, CCBVand; cbv_or, CCBVor; cbv_xor, CCBVxor; + cbv_add, CCBVadd; cbv_mult, CCBVmult; + cbv_ult, CCBVult; cbv_slt, CCBVslt; cbv_concat, CCBVconcat; + cbv_shl, CCBVshl; cbv_shr, CCBVshr; + ceqb,CCeqb; ceqbP,CCeqbP; ceqbZ, CCeqbZ; cbv_eq, CCeqbBV; + cselect, CCselect; cdiff, CCdiff; + cstore, CCstore; + cequalarray, CCeqbA; ]; tbl let op_tbl = lazy (op_tbl ()) - let of_coq ?hash:(h=false) rt ro reify env sigma c = + + let split_list_at n l = + let rec aux acc n l = match n, l with + | 0, _ -> List.rev acc, l + | _, [] -> assert false + | _, x :: l -> aux (x :: acc) (n-1) l + in + aux [] n l + + + let get_coq_term_op = + Hashtbl.find op_coq_terms + + + let of_coq ?hash:(h=false) rt ro reify known_logic env sigma c = let op_tbl = Lazy.force op_tbl in let get_cst c = - try Hashtbl.find op_tbl c with Not_found -> CCunknown in + try + let cc = Hashtbl.find op_tbl c in + if SL.subset (logic_coq_cst cc) known_logic then cc + else CCunknown_deps (gobble_of_coq_cst cc) + with Not_found -> CCunknown + in let rec mk_hatom h = let c, args = Term.decompose_app h in match get_cst c with - | CCxH -> mk_cop CO_xH - | CCZ0 -> mk_cop CO_Z0 + | CCxH -> mk_cop CCxH args + | CCZ0 -> mk_cop CCZ0 args + | CCBV -> mk_cop CCBV args | CCxO -> mk_uop UO_xO args | CCxI -> mk_uop UO_xI args | CCZpos -> mk_uop UO_Zpos args | CCZneg -> mk_uop UO_Zneg args | CCZopp -> mk_uop UO_Zopp args + | CCBVbitOf -> mk_bvbitof args + | CCBVnot -> mk_bvnot args + | CCBVneg -> mk_bvneg args | CCZplus -> mk_bop BO_Zplus args | CCZminus -> mk_bop BO_Zminus args | CCZmult -> mk_bop BO_Zmult args @@ -565,25 +1043,79 @@ module Atom = | CCZle -> mk_bop BO_Zle args | CCZge -> mk_bop BO_Zge args | CCZgt -> mk_bop BO_Zgt args - | CCeqb -> mk_teq Tbool args - | CCeqbP -> mk_teq Tpositive args - | CCeqbZ -> mk_teq TZ args - | CCunknown -> let ty = Retyping.get_type_of env sigma h in - mk_unknown c args ty + | CCBVand -> mk_bop_bvand args + | CCBVor -> mk_bop_bvor args + | CCBVxor -> mk_bop_bvxor args + | CCBVadd -> mk_bop_bvadd args + | CCBVmult -> mk_bop_bvmult args + | CCBVult -> mk_bop_bvult args + | CCBVslt -> mk_bop_bvslt args + | CCBVconcat -> mk_bop_bvconcat args + | CCBVextr -> mk_bvextr args + | CCBVzextn -> mk_bvzextn args + | CCBVsextn -> mk_bvsextn args + | CCBVshl -> mk_bop_bvshl args + | CCBVshr -> mk_bop_bvshr args + | CCeqb -> mk_bop (BO_eq Tbool) args + | CCeqbP -> mk_bop (BO_eq Tpositive) args + | CCeqbZ -> mk_bop (BO_eq TZ) args + | CCeqbA -> mk_bop_farray_equal args + | CCeqbBV -> mk_bop_bveq args + | CCselect -> mk_bop_select args + | CCdiff -> mk_bop_diff args + | CCstore -> mk_top_store args + | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) + | CCunknown_deps gobble -> + mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble + + + and mk_cop op args = match op, args with + | CCxH, [] -> get reify (Acop CO_xH) + | CCZ0, [] -> get reify (Acop CO_Z0) + | CCBV, [bs] -> get reify (Acop (CO_BV (mk_bool_list bs))) + | _ -> assert false - and mk_cop op = get reify (Acop op) and mk_uop op = function - | [a] -> let h = mk_hatom a in get reify (Auop (op,h)) - | _ -> failwith "unexpected number of arguments for mk_uop" - - and mk_teq ty args = - if h then match args with - | [a1; a2] -> let h1 = mk_hatom a1 in - let h2 = mk_hatom a2 in - mk_eq reify true ty h1 h2 - | _ -> failwith "unexpected number of arguments for mk_teq" - else mk_bop (BO_eq ty) args + | [a] -> let h = mk_hatom a in + get reify (Auop (op,h)) + | _ -> assert false + + and mk_bvbitof = function + | [s;n;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVbitOf (mk_bvsize s, mk_nat n), h)) + | _ -> assert false + + and mk_bvnot = function + | [s;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVnot (mk_bvsize s), h)) + | _ -> assert false + + and mk_bvneg = function + | [s;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVneg (mk_bvsize s), h)) + | _ -> assert false + + and mk_bvextr = function + | [i;n;s;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVextr (mk_N i, mk_N n, mk_bvsize s), h)) + | _ -> assert false + + and mk_bvzextn = function + | [s;n;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVzextn (mk_bvsize s, mk_N n), h)) + | _ -> assert false + + and mk_bvsextn = function + | [s;n;a] -> + let h = mk_hatom a in + get reify (Auop (UO_BVsextn (mk_bvsize s, mk_N n), h)) + | _ -> assert false and mk_bop op = function | [a1;a2] -> @@ -592,19 +1124,148 @@ module Atom = get reify (Abop (op,h1,h2)) | _ -> failwith "unexpected number of arguments for mk_bop" + and mk_top op = function + | [a1;a2;a3] -> + let h1 = mk_hatom a1 in + let h2 = mk_hatom a2 in + let h3 = mk_hatom a3 in + get reify (Atop (op,h1,h2,h3)) + | _ -> assert false + + and mk_bop_bvand = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVand s') [a1;a2] + | _ -> assert false + + and mk_bop_bvor = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVor s') [a1;a2] + | _ -> assert false + + and mk_bop_bvxor = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVxor s') [a1;a2] + | _ -> assert false + + and mk_bop_bvadd = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVadd s') [a1;a2] + | _ -> assert false + + and mk_bop_bvmult = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVmult s') [a1;a2] + | _ -> assert false + + and mk_bop_bvult = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVult s') [a1;a2] + | _ -> assert false + + and mk_bop_bvslt = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVslt s') [a1;a2] + | _ -> assert false + + and mk_bop_bvshl = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVshl s') [a1;a2] + | _ -> assert false + + and mk_bop_bvshr = function + | [s;a1;a2] -> + let s' = mk_bvsize s in + mk_bop (BO_BVshr s') [a1;a2] + | _ -> assert false + + and mk_bop_bvconcat = function + | [s1;s2;a1;a2] -> + mk_bop (BO_BVconcat (mk_bvsize s1, mk_bvsize s2)) [a1;a2] + | _ -> assert false + + and mk_bop_bveq = function + | [s;a1;a2] when SL.mem LBitvectors known_logic -> + let s' = mk_bvsize s in + mk_bop (BO_eq (TBV s')) [a1;a2] + (* We still want to interpret bv equality as uninterpreted + smtlib2 equality if the solver doesn't support bitvectors *) + | [s;a1;a2] -> + let ty = SmtBtype.of_coq rt known_logic (mklApp cbitvector [|s|]) in + mk_bop (BO_eq ty) [a1;a2] + | _ -> assert false + + and mk_bop_select = function + | [ti;te;_;_;_;a;i] -> + let ti' = SmtBtype.of_coq rt known_logic ti in + let te' = SmtBtype.of_coq rt known_logic te in + mk_bop (BO_select (ti', te')) [a; i] + | _ -> assert false + + and mk_bop_diff = function + | [ti;te;_;_;_;_;_;_;_;_;a;b] -> + let ti' = SmtBtype.of_coq rt known_logic ti in + let te' = SmtBtype.of_coq rt known_logic te in + mk_bop (BO_diffarray (ti', te')) [a; b] + | _ -> assert false + + and mk_top_store = function + | [ti;te;_;_;_;_;_;_;a;i;e] -> + let ti' = SmtBtype.of_coq rt known_logic ti in + let te' = SmtBtype.of_coq rt known_logic te in + mk_top (TO_store (ti', te')) [a; i; e] + | _ -> assert false + + and mk_bop_farray_equal = function + | [ti;te;_;_;_;_;_;a;b] when SL.mem LArrays known_logic -> + let ti' = SmtBtype.of_coq rt known_logic ti in + let te' = SmtBtype.of_coq rt known_logic te in + mk_bop (BO_eq (TFArray (ti', te'))) [a; b] + (* We still want to interpret array equality as uninterpreted + smtlib2 equality if the solver doesn't support arrays *) + | [ti;te;ord_ti;_;_;_;inh_te;a;b] -> + let ty = SmtBtype.of_coq rt known_logic + (mklApp cfarray [|ti; te; ord_ti; inh_te|]) in + mk_bop (BO_eq ty) [a;b] + | _ -> assert false + and mk_unknown c args ty = let hargs = Array.of_list (List.map mk_hatom args) in - let op = try Op.of_coq ro c - with Not_found -> - let targs = Array.map type_of hargs in - let tres = SmtBtype.of_coq rt ty in - let os = if Term.isRel c - then let i = Term.destRel c in - let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in - Some (string_of_name n) - else None in - Op.declare ro c targs tres os in - get reify (Aapp (op,hargs)) in + let op = + try Op.of_coq ro c + with | Not_found -> + let targs = Array.map type_of hargs in + let tres = SmtBtype.of_coq rt known_logic ty in + let os = if Term.isRel c then + let i = Term.destRel c in + let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in + Some (string_of_name n) + else + None + in + Op.declare ro c targs tres os in + (try + let (i, _) = destruct "" op in + Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *) + with | Failure _ -> ()); + get reify (Aapp (op,hargs)) + + (* create an uninterpreted symbol for an unsupported symbol but fisrt do + partial application to its dependent arguments whose number is given by + [gobble] *) + and mk_unknown_deps c args ty gobble = + let deps, args = split_list_at gobble args in + let c = Term.mkApp (c, Array.of_list deps) in + mk_unknown c args ty + + in mk_hatom c @@ -616,15 +1277,21 @@ module Atom = | Acop op -> mklApp cAcop [|Op.c_to_coq op|] | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|] | Abop (op,h1,h2) -> - mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|] + mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|] + | Atop (op,h1,h2,h3) -> + mklApp cAtop [|Op.t_to_coq op;to_coq h1; to_coq h2; to_coq h3|] | Anop (op,ha) -> - let cop = Op.n_to_coq op in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in - mklApp cAnop [|cop; cargs|] + let cop = Op.n_to_coq op in + let cargs = Array.fold_right + (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) + ha (mklApp cnil [|Lazy.force cint|]) in + mklApp cAnop [|cop; cargs|] | Aapp (op,args) -> - let cop = Op.i_to_coq op in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in - mklApp cAapp [|cop; cargs|] + let cop = Op.i_to_coq op in + let cargs = Array.fold_right + (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) + args (mklApp cnil [|Lazy.force cint|]) in + mklApp cAapp [|cop; cargs|] let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |]) @@ -640,22 +1307,30 @@ module Atom = (** Producing a Coq term corresponding to the interpretation of an atom *) - let interp_to_coq atom_tbl a = + let interp_to_coq t_i atom_tbl a = let rec interp_atom a = let l = index a in try Hashtbl.find atom_tbl l with Not_found -> let pc = match atom a with - | Acop c -> Op.interp_cop c - | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) - | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|]) - | Anop (NO_distinct ty as op,ha) -> - let cop = Op.interp_nop op in - let typ = Op.interp_distinct ty in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Term.mkApp (cop,[|cargs|]) - | Aapp ((_, hval),t) -> Term.mkApp (hval.op_val, Array.map interp_atom t) in + | Acop c -> Op.interp_cop c + | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Abop (op,h1,h2) -> + Term.mkApp (Op.interp_bop t_i op, + [|interp_atom h1; interp_atom h2|]) + | Atop (op,h1,h2,h3) -> + Term.mkApp (Op.interp_top t_i op, + [|interp_atom h1; interp_atom h2; interp_atom h3|]) + | Anop (NO_distinct ty as op,ha) -> + let cop = Op.interp_nop t_i op in + let typ = SmtBtype.interp t_i ty in + let cargs = Array.fold_right (fun h l -> + mklApp ccons [|typ; interp_atom h; l|]) + ha (mklApp cnil [|typ|]) in + Term.mkApp (cop,[|cargs|]) + | Aapp (op,t) -> + Term.mkApp ((snd op).op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a @@ -663,11 +1338,13 @@ module Atom = (* Generation of atoms *) - let mk_nop op reify ?declare:(decl=true) a = get ~declare:decl reify (Anop (op,a)) + let mk_nop ?declare:(decl=true) op reify a = get ~declare:decl reify (Anop (op,a)) + + let mk_binop ?declare:(decl=true) op reify h1 h2 = get ~declare:decl reify (Abop (op, h1, h2)) - let mk_binop op reify decl h1 h2 = get ~declare:decl reify (Abop (op, h1, h2)) + let mk_terop ?declare:(decl=true) op reify h1 h2 h3 = get ~declare:decl reify (Atop (op, h1, h2, h3)) - let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h)) + let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h)) let rec hatom_pos_of_int reify i = if i <= 1 then @@ -702,19 +1379,57 @@ module Atom = if Big_int.gt_big_int i Big_int.zero_big_int then mk_unop UO_Zpos reify (hatom_pos_of_bigint reify i) else - mk_unop UO_Zneg reify (hatom_pos_of_bigint reify (Big_int.minus_big_int i)) - - let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h)) - - let mk_lt = mk_binop BO_Zlt - let mk_le = mk_binop BO_Zle - let mk_gt = mk_binop BO_Zgt - let mk_ge = mk_binop BO_Zge - let mk_plus = mk_binop BO_Zplus - let mk_minus = mk_binop BO_Zminus - let mk_mult = mk_binop BO_Zmult - let mk_opp = mk_unop UO_Zopp - let mk_distinct reify ty = mk_nop (NO_distinct ty) reify + mk_unop UO_Zneg reify + (hatom_pos_of_bigint reify (Big_int.minus_big_int i)) + + let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h)) + + let mk_lt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zlt ra + let mk_le ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zle ra + let mk_gt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zgt ra + let mk_ge ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zge ra + let mk_plus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zplus ra + let mk_minus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zminus ra + let mk_mult ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zmult ra + let mk_bvand reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVand s) reify + let mk_bvor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVor s) reify + let mk_bvxor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVxor s) reify + let mk_bvadd reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVadd s) reify + let mk_bvmult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVmult s) reify + let mk_bvult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVult s) reify + let mk_bvslt reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVslt s) reify + let mk_bvconcat reify ?declare:(decl=true) s1 s2 = mk_binop ~declare:decl (BO_BVconcat (s1, s2)) reify + let mk_opp ra ?declare:(decl=true) = mk_unop ~declare:decl UO_Zopp ra + let mk_distinct reify ?declare:(decl=true) ty = mk_nop ~declare:decl (NO_distinct ty) reify + let mk_bitof reify ?declare:(decl=true) s i = mk_unop ~declare:decl (UO_BVbitOf (s, i)) reify + let mk_bvnot reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVnot s) reify + let mk_bvneg reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVneg s) reify + let mk_bvconst reify bool_list = get reify (Acop (CO_BV bool_list)) + let mk_select reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_select (ti, te)) reify + let mk_diffarray reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_diffarray (ti, te)) reify + let mk_store reify ?declare:(decl=true) ti te = mk_terop ~declare:decl (TO_store (ti, te)) reify + let mk_bvextr reify ?declare:(decl=true) ~i ~n ~s = mk_unop ~declare:decl (UO_BVextr (i, n, s)) reify + let mk_bvzextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVzextn (s, n)) reify + let mk_bvsextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVsextn (s, n)) reify + let mk_bvshl reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshl s) reify + let mk_bvshr reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshr s) reify + + + let rec logic_atom = function + | Acop c -> Op.logic_of_cop c + | Auop (u, h) -> SL.union (Op.logic_of_uop u) (logic h) + | Abop (b, h1, h2) -> + SL.union (Op.logic_of_bop b) (SL.union (logic h1) (logic h2)) + | Atop (t, h1, h2, h3) -> + SL.union (Op.logic_of_top t) + (SL.union (logic h1) (SL.union (logic h2) (logic h3))) + | Anop (n, ha) -> + Array.fold_left (fun l h -> SL.union (logic h) l) (Op.logic_of_nop n) ha + | Aapp (i, ha) -> + Array.fold_left (fun l h -> SL.union (logic h) l) + (Op.logic_of_indexed i) ha + + and logic h = logic_atom h.hval end @@ -728,9 +1443,13 @@ module Trace = SmtTrace.MakeOpt(Form) let mk_ftype cod dom = let typeb = Lazy.force ctype in let typea = mklApp clist [|typeb|] in - let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in + let a = Array.fold_right + (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|]) + cod (mklApp cnil [|typeb|]) in let b = SmtBtype.to_coq dom in mklApp cpair [|typea;typeb;a;b|] -let make_t_i rt = SmtBtype.interp_tbl rt -let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro +let make_t_i = SmtBtype.make_t_i +let make_t_func ro t_i = + Op.interp_tbl (mklApp ctval [|t_i|]) + (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro -- cgit