Code Monkey home page Code Monkey logo

hipsleek's Introduction

Installation Guide for hip/sleek

Normal Installation

  1. Compile Omega modified as follows:

    cd omega_modified
make oc

    The omega executable is now in omega_calc/obj/oc. Please move it to some default location, such as /usr/local/bin.

  2. Compile Mona as follows:

    tar -xvf mona-1.4-modif.tar.gz
cd mona-1.4
./install.sh

    The mona executable is now placed in /usr/local/bin.

  3. Please install latest Ocaml compiler in your directory. Please also install Coq prover.

  4. You are now ready to install hip/sleek, as follows:

    cd ..
make

The executables `hip` and `sleek` can now be used (or moved
to `/usr/local/bin`)

  5. Sleek examples can be found in examples/working/sleek subdirectory. You can test it as follows:

    1. Entailment using default Omega

      ./sleek examples/working/sleek/sleek2.slk

    2. Entailment using Mona

      ./sleek -tp mona examples/working/sleek/sleek2.slk

    3. Verification using default Omega

      ./hip examples/working/hip/ll.ss

    4. Verification using Mona

      ./hip -tp mona examples/working/hip/ll.ss

Installation with hipsleek/dependencies

This process should work on an Ubuntu-like system.

  1. Clone this repository with git clone --recursive https://github.com/hipsleek/dependencies.
  2. Install hipsleek/dependencies.
  3. Install hipsleek/hipsleek.

Omega for MAC:

(by Yahui Song, 25th May 2020, [email protected], email me if you have difficulties compiling on mac)

  1. uncompress this omega_modified_for_mac.zip folder and use it to replace your omega_modified folder under sleekex/
  2. run 
    cd omega_modified
  make depend
cd omega_calc/obj
make
sudo cp oc /usr/local/bin/
  3. and then you go back and make the sleekex again.

hipsleek's People

Contributors

chinwn avatar lequangloc avatar letonchanh avatar andrecostea avatar taquangtrung avatar trinhmt avatar zhengqunkoo avatar benedictleejh avatar thanhtoantnt avatar ngjiewu avatar thisisadiyoga avatar songyahui avatar hipsleek1 avatar fadisng avatar enenyi avatar

hipsleek's Issues

Analysis of entailments with issues

The following table shows results of ./sleek -dre="compute_pretty_actions\|isFailCtx" --pnum <pnum> <filename> | ./remove-aliases.py | less, at commit 5edb3fc.

If table is too wide, please scroll horizontally.

<pnum> checkentail search comments <filename> issue function@call entailment pretty entailment simplified pretty entailment
15 checkentail x::arr_seg<5> & y=x+1 |- x::arr_seg<1> * y::int_arr_seg<1>. SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] Unable to instantiate q_293=1+x, b_291=4, a_292=1. Unable to either indirectly fold int_arr_seg<1> into arr_seg<4>, or do so directly via lemma "int2char". testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@14 q_293::arr_seg<b_291>@M & flted_156_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=1+x & flted_156_270=5 |- y::int_arr_seg<flted_157_288>@M & flted_157_289=1 & flted_157_288=1 q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=5 |- 1+x::int_arr_seg<1>@M 1+x::arr_seg<4>@M & Univ(1+x) |- 1+x::int_arr_seg<1>@M
16 checkentail x::arr_seg<4*n+1> & y=x+4*n |- x::arr_seg<4*n> * y::arr_seg<1>. SEARCH =>[SEARCH =>[COND =>[Match, COND =>[BaseCaseFold, BaseCaseUnfold]], (Lemma 0==> splitchar_left), (Lemma 0<== splitchar_left_right)]] Entailment is due to function@call compute_pretty_actions@7 with action (Lemma 0<== int2char_left_right) on LHS: x::arr_seg<1+(4*n)>@M and RHS: x::int_arr_seg<n_289>@M, which should give x::arr_seg<1+(4*n)>@M |- x::arr_seg<4*n>@M * (4*n)+x::arr_seg<1>@M, but (4*n)+x::arr_seg<1>@M is missing from the pretty entailment. This missing heap state appears to be a cosmetic error, since function@call compute_pretty_actions@32 attempts to prove (4*n)+x::arr_seg<1>@M. testcases/ex5c.slk NA compute_pretty_actions@10 x::arr_seg<flted_166_270>@M & flted_166_270=1+(4*n) & y=(4*n)+x |- x::arr_seg<flted_16_296>@M & flted_16_296=4*n_289 x::arr_seg<1+(4*n)>@M |- x::arr_seg<4*n_289>@M NA
16 checkentail x::arr_seg<4*n+1> & y=x+4*n |- x::arr_seg<4*n> * y::arr_seg<1>. SEARCH =>[SEARCH =>[COND =>[Match, COND =>[BaseCaseFold, BaseCaseUnfold]], (Lemma 0==> splitchar_left), (Lemma 0<== splitchar_left_right)]] Unable to instantiate q_302=(4*n)+x, b_300=1, n_289=n. Fails since n_289=n is unprovable, since the antecedent does not have Univ(n_289). It is likely that isFailCtx@33 explains exactly why n_289=n cannot be proved. testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@32 q_302::arr_seg<b_300>@M & a_301=4*n_289 & y=(4*n)+x & flted_166_270=1+(4*n) & Univ(q_302) & Univ(a_301) & Univ(b_300) & a_301+x=q_302 & flted_166_270=b_300+a_301 |- y::arr_seg<flted_167_290>@M & flted_167_290=1 & n_289=n q_302::arr_seg<b_300>@M & 4*n_289=4*n & Univ(q_302) &Univ(4*n_289) & Univ(b_300) & 4*n_289+x=q_302 & 1+(4*n)=b_300+4*n_289 |- (4*n)+x::arr_seg<1>@M 4*n+x::arr_seg<1>@M |- (4*n)+x::arr_seg<1>@M
17 checkentail x::arr_seg<4*n+1> & y=x+1 |- x::arr_seg<1> * y::int_arr_seg<n>. SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] Unable to instantiate q_293=1+x, b_291=4*n, a_292=1. Fails since n_288=n is unprovable, since the antecedent does not have Univ(n_288). Unable to either indirectly fold int_arr_seg<n> into arr_seg<4*n>, or do so directly via lemma "int2char". testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@14 q_293::arr_seg<b_291>@M & flted_178_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=1+x & flted_178_270=1+(4*n) |- y::int_arr_seg<n_288>@M & flted_179_289=1 & n_288=n q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=1+(4*n) |- 1+x::int_arr_seg<n>@M 1+x::arr_seg<4*n>@M |- 1+x::int_arr_seg<n>@M
19 checkentail x::arr_seg<6> & y=x+1 & z=y+4 |- x::arr_seg<1> * y::int_arr_seg<1> * z::arr_seg<1>. SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] Unable to instantiate q_301=1+x, b_299=5, a_300=1. Instantiation of b_299=5 could be helped if information that a_300=1 were provided. Missing information that a_300=1, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_300> and RHS: x::arr_seg<1>. testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@14 q_301::arr_seg<b_299>@M & flted_196_270=b_299+a_300 & a_300+x=q_301 & Univ(b_299) & Univ(a_300) & Univ(q_301) & z=4+y & y=1+x & flted_196_270=6 |- y::int_arr_seg<flted_197_296>@M * z::arr_seg<flted_197_295>@M & flted_197_297=1 & flted_197_296=1 & flted_197_295=1 q_301::arr_seg<b_299>@M & a_300+x=q_301 & Univ(b_299) & Univ(a_300) &Univ(q_301) & 4+y=4+1+x & b_299+a_300=6 |- 1+x::int_arr_seg<1>@M * 4+y::arr_seg<1>@M 1+x::arr_seg<5>@M |- 1+x::int_arr_seg<1>@M * 4+1+x::arr_seg<1>@M
20 checkentail x::arr_seg<6> & y=x+2 |- x::arr_seg<2> * y::int_arr_seg<1>. SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] Unable to instantiate q_293=2+x, b_291=4, a_292=2. Instantiation of b_291=4 could be helped if information that a_292=2 were provided. Missing information that a_292=2, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_292> and RHS: x::arr_seg<2>. Unable to either indirectly fold int_arr_seg<1> into arr_seg<4>, or do so directly via lemma "int2char". testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@14 q_293::arr_seg<b_291>@M & flted_204_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=2+x & flted_204_270=6 |- y::int_arr_seg<flted_205_288>@M & flted_205_289=2 & flted_205_288=1 q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=6 |- 2+x::int_arr_seg<1>@M 2+x::arr_seg<4>@M |- 2+x::int_arr_seg<1>@M
22 checkentail x::arr_seg<4*n+2> & y=x+1 & z=y+4*n |- x::arr_seg<1> * y::int_arr_seg<n> * z::arr_seg<1>. SEARCH =>[COND =>[Match, BaseCaseFold, BaseCaseUnfold]] Entailment is due to function@call compute_pretty_actions@14 with action (Lemma 0<== int2char_left_right) on LHS: q_302::arr_seg<b_300>@M and RHS: y::int_arr_seg<n_296>@M, which should give 1+x::arr_seg<(4*n)+1>@M & (4*n)+y=(4*n)+1+x |- 1+x::arr_seg<4*n_296>@M * (4*n)+y::arr_seg<1>@M, but (4*n)+y::arr_seg<1>@M is missing from the pretty entailment. testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@17 q_302::arr_seg<b_300>@M & a_301=1 & flted_222_270=2+(4*n) & y=1+x & z=(4*n)+y & Univ(q_302) & Univ(a_301) & Univ(b_300) & a_301+x=q_302 & flted_222_270=b_300+a_301 |- y::arr_seg<flted_16_311>@M & flted_16_311=4*n_296 q_302::arr_seg<b_300>@M & (4*n)+y=(4*n)+1+x & Univ(q_302) &Univ(1) & Univ(b_300) & 1+x=q_302 & 2+(4*n)=b_300+1 |- 1+x::arr_seg<4*n_296>@M 1+x::arr_seg<(4*n)+1>@M & (4*n)+y=(4*n)+1+x |- 1+x::arr_seg<4*n_296>@M
23 checkentail x::arr_seg<4*n+2> & y=x+2 |- x::arr_seg<2> * y::int_arr_seg<n>. SEARCH =>[COND =>[BaseCaseFold, UnmatchedRHSData]] Unable to instantiate q_293=2+x, b_291=4*n, a_292=2. Instantiation of b_291=4*n could be helped if information that a_292=2 were provided. Missing information that a_292=2, which hipsleek should have derived and kept in the pretty entailment due to function@call compute_pretty_actions@13 with action Match on LHS: x::arr_seg<a_292> and RHS: x::arr_seg<2>. Unable to either indirectly fold int_arr_seg<n> into arr_seg<4*n>, or do so directly via lemma "int2char". Fails since n_288=n is unprovable, since the antecedent does not have Univ(n_288). testcases/ex5c.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@14 q_293::arr_seg<b_291>@M & flted_230_270=b_291+a_292 & a_292+x=q_293 & Univ(b_291) & Univ(a_292) & Univ(q_293) & y=2+x & flted_230_270=2+(4*n) |- y::int_arr_seg<n_288>@M & flted_231_289=2 & n_288=n q_293::arr_seg<b_291>@M & a_292+x=q_293 & Univ(b_291) & Univ(a_292) &Univ(q_293) & b_291+a_292=2+(4*n) |- 2+x::int_arr_seg<n>@M 2+x::arr_seg<4*n>@M |- 2+x::int_arr_seg<n>@M
13 checkentail a::aseg<a+3> & b=a+1 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+3>. SEARCH =>[UnmatchedRHSData] Either unable to instantiate k_268=1 or unable to instantiate v_278=v. Claims 1+a::int_star<v>@M is UnmatchedRHSData when it is not. testcases/exist-arrays.slk satisfiable state became hfalse compute_pretty_actions@90 b_269::int_star<v_270>@M * c_268::aseg<flted_17_275>@M & flted_17_275=n_266+a & flted_123_105=n_266+a & b_269=k_267+a & c_268=1+b_269 & Univ(v_270) & Univ(n_266) & Univ(k_267) & Univ(c_268) & Univ(b_269) & Univ(v_270) & c=1+b & b=1+a & flted_123_105=3+a |- b::int_star<v>@M * c::aseg<flted_123_126>@M & flted_123_126=3+a & b_125=b k_268+a::int_star<v_278>@M * 1+b_270::aseg<n_267+a>@M &1+b_270=1+k_268+a & Univ(v_278) & Univ(n_267) & Univ(k_268) & Univ(1+b_270) & Univ(k_268+a) & n_267+a=3+a |- 1+a::int_star<v>@M * 1+1+a::aseg<3+a>@M 1+a::int_star<v_278>@M * 1+1+a::aseg<3+a>@M & Univ(v_278) |- 1+a::int_star<v>@M * 1+1+a::aseg<3+a>@M
16 checkentail a::aseg<a+4> & b=a+1 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+4>. SEARCH =>[UnmatchedRHSData] Either unable to instantiate k_270=1 or unable to instantiate v_280=v. Claims 1+a::int_star<v>@M is UnmatchedRHSData when it is not. testcases/exist-arrays.slk satisfiable state became hfalse compute_pretty_actions@92 b_270::int_star<v_271>@M * c_269::aseg<flted_17_276>@M & flted_17_276=n_267+a & flted_144_105=n_267+a & b_270=k_268+a & c_269=1+b_270 & Univ(v_271) & Univ(n_267) & Univ(k_268) & Univ(c_269) & Univ(b_270) & Univ(v_271) & c=1+b & b=1+a & flted_144_105=4+a |- b::int_star<v>@M * c::aseg<flted_144_126>@M & flted_144_126=4+a & b_125=b k_270+a::int_star<v_280>@M * 1+b_272::aseg<n_269+a>@M & Univ(v_280) &1+b_272=1+k_270+a & Univ(n_269) & Univ(k_270) & Univ(1+b_272) & Univ(k_270+a) & n_269+a=4+a |- 1+a::int_star<v>@M * 1+1+a::aseg<4+a>@M 1+a::int_star<v_280>@M * 1+1+a::aseg<4+a>@M & Univ(v_280) |- 1+a::int_star<v>@M * 1+1+a::aseg<4+a>@M
17 checkentail a::aseg<a+4> & b=a+2 & c=b+1 |- a::aseg<b> * b::int_star<v> * c::aseg<a+4>. SEARCH =>[UnmatchedRHSData] Either unable to instantiate k_157=2 or unable to instantiate v_142=v. Claims 3+a::int_star<v>@M is UnmatchedRHSData when it is not. testcases/exist-arrays.slk satisfiable state became hfalse compute_pretty_actions@24 b_163::int_star<v_164>@M * c_162::aseg<flted_17_169>@M & flted_17_169=n_160+a & flted_151_105=n_160+a & b_163=k_161+a & c_162=1+b_163 & Univ(v_164) & Univ(n_160) & Univ(k_161) & Univ(c_162) & Univ(b_163) & Univ(v_164) & c=1+b & b=2+a & flted_151_105=4+a |- b::int_star<v>@M * c::aseg<flted_151_126>@M & flted_151_126=4+a & b_125=b k_157+a::int_star<v_160>@M * 1+b_159::aseg<n_156+a>@M &1+b_159=1+k_157+a & Univ(v_160) & Univ(n_156) & Univ(k_157) & Univ(1+b_159) &Univ(k_157+a) & Univ(v_160) & n_156+a=4+a |- 2+a::int_star<v>@M * 1+2+a::aseg<4+a>@M 2+a::int_star<v_160>@M * 1+2+a::aseg<4+a>@M & Univ(v_160) |- 2+a::int_star<v>@M * 1+2+a::aseg<4+a>@M
18 checkentail a::aseg<a+4> & b=a+3 |- a::aseg<b> * b::int_star<v>. SEARCH =>[UnmatchedRHSData] Either unable to instantiate k_132=3 or unable to instantiate v_142=v. Claims 3+a::int_star<v>@M is UnmatchedRHSData when it is not. testcases/exist-arrays.slk Expecting(3)Valid BUT got : Fail_May compute_pretty_actions@15 b_143::int_star<v_144>@M * c_142::aseg<flted_17_149>@M & flted_17_149=n_140+a & flted_158_105=n_140+a & b_143=k_141+a & c_142=1+b_143 & Univ(v_144) & Univ(n_140) & Univ(k_141) & Univ(c_142) & Univ(b_143) & Univ(v_144) & b=3+a & flted_158_105=4+a |- b::int_star<v>@M & b_118=b k_132+a::int_star<v_142>@M * 1+b_134::aseg<n_131+a>@M &1+b_134=1+k_132+a & Univ(v_142) & Univ(n_131) & Univ(k_132) & Univ(1+b_134) & Univ(k_132+a) & n_131+a=4+a |- 3+a::int_star<v>@M 3+a::int_star<v_142>@M * 1+3+a::aseg<4+a>@M & Univ(v_142) |- 3+a::int_star<v>@M

Fix of #1 is incomplete

issues-1.slk.iget_answer.rec at commit c937a7f probably has the correct ouput by chance, because 2e37560 has a bug that is not manifested: when (reset) is used, the input to Z3 is, given by new_f at line

hipsleek/smtsolver.ml

Line 751 in 2e37560

let new_f = "(push)\n" ^ f ^ "(pop)\n" in
, as in:

(push)
(reset)
;Variables declarations
(declare-fun n () Int)
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (< 1 n))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (<= 2 f))
;Negation of Consequence
(assert (not (exists ((alpha_134 Int)) (= (* 2 alpha_134) f))))
(check-sat)(pop)

on which running z3 -smt2 gives:

unsat
(error "line 14 column 15: invalid pop command, argument is greater than the current stack depth")

which could have unintended consequences. The solution is to remove (push) and (pop) from new_f whenever (reset) is used. A similar problem likely manifests at new_f at line

hipsleek/smtsolver.ml

Line 1313 in 2e37560

let new_f = if not is_opt then "(push)\n" ^ f ^ "(pop)\n" else f in
.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.