Delta-Debugging of Constraints

[ranjitjhala]

We should merge the code here:

https://github.com/rolph-recto/liquidhaskell/blob/fault-local/FaultLocal.hs

by @rolph-recto into liquid-fixpoint (not in LH), this should help with debugging fixpoint itself (and of course, better error messages for LH, RefScript et al.

[BenjaminCosman]

@rolph-recto what commit of Fixpoint does that build with?

[ranjitjhala]

I'm going to do this now.

[rolph-recto]

Sorry, somehow I missed this issue!

I've migrated the delta debugging code here: https://github.com/rolph-recto/liquid-fixpoint/tree/fault-local-mainline

You can see the relevant changes in this commit log: https://github.com/rolph-recto/liquid-fixpoint/commit/6ae951cc1f5135d1533de188fd97fee49ffdadf5

Basically solveFaultLocal partitions FInfo a and runs delta debugging on failing partitions, using solve as a type-checking oracle. It returns a concatenated set from each minimal failing constraint set found in failing partitions.

I haven't had a chance to test it since the interface for fault localization is to be decided -- will meet with @ranjitjhala later today to figure this out.

(By the way the parent of this commit is b6ffad54849e90ec8d3af088fb2e1d4c1bf4179a, which is the commit that ucsd-progsys/liquid-fixpoint/master is pointing to as of 11/13/15 15:20 EST / 12:20 PST.)

[rolph-recto]

Ok, added command line options to call minimization and write minimized FInfo to a new fq file. The commit is here.

However, I get this error message when I try to run minimization on an fq file:

$ ./fixpoint --minimize test2.fq

Liquid-Fixpoint Copyright 2013-15 Regents of the University of California.
All Rights Reserved.
fixpoint: ./.liquid/test2.fq.1.smt2: openFile: resource busy (file is locked)

It looks like it hangs when solve is called because the previous call to solve still has the lock on the smt file that interfaces with the solver. Any ideas on how to prevent this from happening? My previous implementations of minimizeFQ, which is pretty much the same as it is here, never ran into this problem.

Also @ranjitjhala: I tried writing the minimization code in a separate module like you've suggested, but there are mutual dependencies between solve and minimizeFQ so that it's impossible to do so. All of the code then has to live in Interface.hs, unfortunately.

[ranjitjhala]

Is this based off master?

On Dec 3, 2015, at 9:01 PM, Rolph Recto notifications@github.com wrote:

Ok, added command line options to call minimization and write minimized FInfo to a new fq file. The commit is here.

However, I get this error message when I try to run minimization on an fq file:

$ ./fixpoint --minimize test2.fq

Liquid-Fixpoint Copyright 2013-15 Regents of the University of California. All Rights Reserved. fixpoint: ./.liquid/test2.fq.1.smt2: openFile: resource busy (file is locked) It looks like it hangs when solve is called because the previous call to solve still has the lock on the smt file that interfaces with the solver. Any ideas on how to prevent this from happening? My previous implementations of minimizeFQ, which is pretty much the same as it is here, never ran into this problem.

Also @ranjitjhala: I tried writing the minimization code in a separate module like you've suggested, but there are mutual dependencies between solve and minimizeFQ so that it's impossible to do so. All of the code then has to live in Interface.hs, unfortunately.

— Reply to this email directly or view it on GitHub.

[rolph-recto]

Yes, specifically https://github.com/ucsd-progsys/liquid-fixpoint/commit/b6ffad54849e90ec8d3af088fb2e1d4c1bf4179a.

[rolph-recto]

@ranjitjhala I revisited this and I think I found the cause of failure: runSolverM gets called multiple times but cleanupContext is not called, leaving the file handle to the *.smt2 file hanging. I modified runSolverM as follows to fix this:

runSolverM cfg fi _ act = do
  ctx <-  makeContext (not $ real cfg) (solver cfg) file
  res <- runStateT (declare fi >> act) (SS ctx be $ stats0 fi)

  -- add the following line to make delta debug minimize work
  cleanupContext ctx
  return $ fst res

And indeed the bug in the above comments goes away. Now a call to fixpoint --minimize [file] will generate .liquid/[file].minfq, which contains only the minimal unsatisfiable constraint set (a subset of the originally fq file).

I manually rebased the minimization code to the current master branch (187a887cbd) of ucsd-progsys/liquid-fixpoint; see the commit here.

[ranjitjhala]

Nice! So I should try to merge the PR now?

On Jan 20, 2016, at 3:14 AM, Rolph Recto notifications@github.com wrote:

@ranjitjhala I revisited this and I think I found the cause of failure: runSolverM gets called multiple times but cleanupContext is not called, leaving the file handle to the *.smt2 file hanging. I modified runSolverM as follows to fix this:

runSolverM cfg fi _ act = do ctx <- makeContext (not $ real cfg) (solver cfg) file res <- runStateT (declare fi >> act) (SS ctx be $ stats0 fi)

-- add the following line to make delta debug minimize work cleanupContext ctx return $ fst res And indeed the bug in the above comments goes away. Now a call to fixpoint --minimize [file] will generate .liquid/[file].minfq, which contains only the minimal unsatisfiable constraint set (a subset of the originally fq file).

I manually rebased the minimization code to the current master branch (187a887) of ucsd-progsys/liquid-fixpoint; see the commit here.

— Reply to this email directly or view it on GitHub.

[gridaphobe]

@rolph-recto cleanupContext won't be run if the smt solver aborts, we probably need to use https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Exception-Base.html#v:bracket instead.

[rolph-recto]

Pull request is here: https://github.com/ucsd-progsys/liquid-fixpoint/pull/183

As per @gridaphobe 's suggestion, I added exception handling code in runSolverM.

[ranjitjhala]

The above or #183 is long merged.