Remove explicit `IO` from our SMT interface #99

VictorCMiraldo · 2022-05-29T19:02:50Z

What

This PR does two large, but intertwined, pieces of work:

Isolates the interface to the SMT solver from the rest of the code, preparing pirouette to interact with a solver through:
```
solve :: SharedContext lang -> Problem lang res -> res
```
In this process, I also used the more modern typed-process to launch the SMT process instead of how SimpleSMT used to do it.
Cleans and refactors a lot of the symbolic evaluation engine

Partially applying something to solve should cause further calls to share that shared context. Here's a gist showing a little experiment I did in this direction: https://gist.github.com/VictorCMiraldo/b7c448bb2bcf4b49962082970d61f64a

It doesn't use that solve function just yet, we need some further cleanup (#106) to start using it. Nevertheless, the interface with the symbolic evaluation engine is already defined in terms of a problem GADT:

data SolverProblem lang :: * -> * where
  CheckProperty :: (LanguagePretty lang) => CheckPropertyProblem lang -> SolverProblem lang PruneResult
  CheckPath :: CheckPathProblem lang -> SolverProblem lang Bool

It is only inside the interpretation of those problems that we interact directly with the solver; anywhere else in the symbolic engine we just call solveProblem for now and in a next PR, will become just solve.

Why

Having an explicit IO monad (or a MonadIO m constraint) simply because we need to talk to an SMT solver is a bad idea. For one, it means we cannot be lazy enough and are always performing more work than we should (#97); Secondly, this implies an unnecessary sentimentality to our backend: why can't we easily explore disjoint branches in parallel?

which will later be handled in an outer unsafePerformIO loop

typed-process instead of the lower level process library.

default.nix and shell.nix here?

broken tests now. Need to investigate

VictorCMiraldo · 2022-06-14T09:01:38Z

The last commit broke our tests. Our session with the solver now only sends empty assert statements:

[send: 120238] (set-option :produce-models true )
[send: 120238] (set-logic ALL )
[send: 120238] (declare-datatype pir_Delta ((pir_D (pir_D_1 Int ) (pir_D_2 Int ) ) ) )
[send: 120238] (declare-fun pir_odd (Int ) Bool )
[send: 120238] (declare-fun pir_even (Int ) Bool )
[send: 120238] (declare-fun pir_and (Bool Bool ) Bool )
[send: 120238] (declare-fun pir_snd (pir_Delta ) Int )
[send: 120238] (declare-fun pir_fst (pir_Delta ) Int )
[send: 120238] (declare-fun pir_ohearn (pir_Delta ) pir_Delta )
[send: 120238] (push 1 )
[send: 120238] (declare-fun pir___result () pir_Delta )
[send: 120238] (declare-fun pir_x () pir_Delta )
[send: 120238] (check-sat )
[recv: 120238] sat
[send: 120238] (pop 1 )
[send: 120238] (push 1 )
[send: 120238] (declare-fun pir___result () pir_Delta )
[send: 120238] (declare-fun pir_s0 () Int )
[send: 120238] (declare-fun pir_s1 () Int )
[send: 120238] (declare-fun pir_s2 () Int )
[send: 120238] (declare-fun pir_s3 () Int )
[send: 120238] (declare-fun pir_x () pir_Delta )
[send: 120238] (assert true ) -- HERE: empty assert!!
[send: 120238] (assert true )
[send: 120238] (check-sat )
[recv: 120238] sat

For the record, this is the same part of the session with the solver from commit 96b78f4 (with the compilation error fixed)

[send: 115976] (set-option :produce-models true )
[send: 115976] (set-logic ALL )
[send: 115976] (declare-datatype pir_Delta ((pir_D (pir_D_1 Int ) (pir_D_2 Int ) ) ) )
[send: 115976] (declare-fun pir_odd (Int ) Bool )
[send: 115976] (declare-fun pir_even (Int ) Bool )
[send: 115976] (declare-fun pir_and (Bool Bool ) Bool )
[send: 115976] (declare-fun pir_snd (pir_Delta ) Int )
[send: 115976] (declare-fun pir_fst (pir_Delta ) Int )
[send: 115976] (declare-fun pir_ohearn (pir_Delta ) pir_Delta )
[send: 115976] (push 1 )
[send: 115976] (declare-fun pir___result () pir_Delta )
[send: 115976] (declare-fun pir_x () pir_Delta )
[send: 115976] (check-sat )
[recv: 115976] sat
[send: 115976] (pop 1 )
[send: 115976] (push 1 )
[send: 115976] (declare-fun pir___result () pir_Delta )
[send: 115976] (declare-fun pir_s0 () Int )
[send: 115976] (declare-fun pir_s1 () Int )
[send: 115976] (declare-fun pir_s2 () Int )
[send: 115976] (declare-fun pir_s3 () Int )
[send: 115976] (declare-fun pir_x () pir_Delta )
[send: 115976] (assert (= pir_x ((as pir_D pir_Delta ) pir_s2 pir_s3 ) ) ) -- HERE: Non-empty assert
[send: 115976] (assert (= pir___result ((as pir_D pir_Delta ) pir_s0 pir_s1 ) ) )
[send: 115976] (check-sat )
[recv: 115976] sat

… can hardly translate anything, leaving us only with empty constraints

VictorCMiraldo · 2022-06-14T11:14:18Z

While stripping everything Pirouette-specific from our API with the SMT solver, I noticed that we rely on PirouetteReadDefs in multiple places, which is perfectly fine. The problem is that PirouetteReadDefs has a few too many dependencies, in particular, the Logger monad and PrtOpts are no longer used, pirouette is not meant as a standalone executable anymore. These should be removed at some point.

0xd34df00d

All looks good, modulo a couple of nitpicks and maybe pushMStack/popMStack stuff.

0xd34df00d · 2022-06-14T15:59:32Z

src/Pirouette/SMT/Constraints.hs

@@ -60,14 +61,15 @@ data Branch lang meta = Branch
    newTerm :: TermMeta lang meta
  }

+-- TODO: Maybe this should be merged with 'LanguageSMT'


Are there (or would there be) any useful instances of LanguageSMT that are not LanguageSMTBranches?

Our implementation requires both instances to run the symbolic evaluation, so I guess it doesn't really matter, any lang must be LanguageSMT lang and LanguageSMTBranches lang.

I'm under the impression that these classes were separated because certain types used inside LanguageSMTBranches are not available where LanguageSMT is at and would require some puzzle solving to find non-cyclical imports to satisfy everything. I decided to leave it untouched for now.

This might be a good moment to rename those classes. The general idea is:

LanguageBuiltins --> defines the built-ins (both terms and types) | \ | LanguageBuiltinTypes --> defines the typing rules of each built-in term | LanguageSMT --> defines translation of built-ins into SMT | (not every term can be translated) | LanguageSMTBranches --> defines at which points the symbolic evaluator has to do sth. special

on that sense, LanguageSMTBranches could well be renamed to LanguageSymEval or something similar.

To give you a difference, the LanguageSMT translation of if ... then ... else ... uses the ifthenelse primitive in Z3. However, the LanguageSMTBranches translation specifies that when an if is found, two new branches must be created:

Add condition = True to the list of known things, continue with the then term,

Add condition = False to the list of known things, continue with the else term.

I won't do that in this PR, I'll do it on the next, which will remove the Logger too. I like LanguageSymEval!

0xd34df00d · 2022-06-14T16:19:04Z

src/Pirouette/SMT/Monadic.hs

+
+-- |If a function can be declared as an uninterpreted function, returns
+-- the type of its arguments and the type of its result.
+supportedUninterpretedFunction ::


What does supported part of the name mean? Does it mean that the type could be converted (judging from the implementation), or something else?

previously, we were using declareAsManyUninterpretedFunctinosAsPossible inside initSolver, and initSolver would return the list of names that managed to be declared. Those that we don't "support", just get silently ignored, which was fine but it adds a dependency between initSolver and everything else.

I split declareAsManyUninterpretedFunctionsAsPossible into two: first give me the list of functions that I know I can declared (because we've managed to translate their types already), then declare then in initSolver. Now, I don't need the result of initSolver to have the set of knownNames.

I'll remove the old declareAsManyUninterpretedFunctionsAsPossible and will update the comment.

(I'll keep this unresolved so the comment is always visible, breaking the data dependencies is an important point of this PR)

src/Pirouette/SMT/Monadic.hs

src/PureSMT.hs

serras · 2022-06-15T07:27:25Z

While stripping everything Pirouette-specific from our API with the SMT solver, I noticed that we rely on PirouetteReadDefs in multiple places, which is perfectly fine. The problem is that PirouetteReadDefs has a few too many dependencies, in particular, the Logger monad and PrtOpts are no longer used, pirouette is not meant as a standalone executable anymore. These should be removed at some point.

This would be very welcome! I've struggled with this in the past, mostly because of PirouetteReadDefs being defined as its own Reader thing, making it difficult to compose with others.

VictorCMiraldo · 2022-06-15T07:28:35Z

@0xd34df00d thanks for the review! I fixed all I could on this iteration and I added a lock to MStack to make sure no race condition can happen. That is untested code and I'll resort to really using it in the next PR; worst case scenario it doesn't work and we postpone relying on the pure solve for a while longer :)

edit: I removed the solve function; it is not used ATM and it should be introduced in its own PR, it's certainly a beast that needs attention

VictorCMiraldo · 2022-06-15T07:29:44Z

This would be very welcome! I've struggled with this in the past, mostly because of PirouetteReadDefs being defined as its own Reader thing, making it difficult to compose with others.

@serras, I hope to do this today!

will bring it on the next one.

Victor Miraldo and others added 7 commits May 29, 2022 20:50

Drafting a separation of the SMT solver API through two functions,

4d89138

which will later be handled in an outer unsafePerformIO loop

hlint

840e096

Merge branch 'dev' into vcm/unsafePerformIO-smt-api

d3ded1a

Refactored SimpleSMT into PureSMT; wrote the backend relying on

2f50a5e

typed-process instead of the lower level process library.

Remove comments from older default.nix; why do we even have

2873fca

default.nix and shell.nix here?

Bring pretty instances out of PureSMT

96b78f4

Removed data dependency between solverInit and solveProblem; have

c4eaa24

broken tests now. Need to investigate

Victor Miraldo added 3 commits June 14, 2022 11:55

Constructor names must also be computed as 'knownNames', otherwise we…

79c2500

… can hardly translate anything, leaving us only with empty constraints

Maybe knownNames should really be a set, we repeatedly do lookups there

f2ff0e1

Switch to using set functions, not Data.Traversable

469f08c

VictorCMiraldo mentioned this pull request Jun 14, 2022

In dev: Remove Logger and rename LanguageSMTBranches #106

Closed

Victor Miraldo added 9 commits June 14, 2022 13:40

Hacking my way around #109

35e2ca1

Split the 'Solve' class from pirouette

151d9f2

Massive refactor part1

0892e2f

Continue the refactor, now starting to remove unused code

888f711

Remove warnings, ormolu pass

0ad18a8

Move Symbolic subfolder out of Term namespace

35859bb

Removed warnings; added comments and TODOS. Getting there

09e814a

Write the infamous pure 'solve' function

f85e2c2

Fix errors; launch the right solver

cb1484a

VictorCMiraldo marked this pull request as ready for review June 14, 2022 15:08

VictorCMiraldo requested review from serras, florentc and 0xd34df00d June 14, 2022 15:08

0xd34df00d approved these changes Jun 14, 2022

View reviewed changes

Victor Miraldo added 2 commits June 15, 2022 08:59

Remove declareUninterpretedFunctions and friends

68ff555

Update comments in PureSMT; add a lock to pushMStack and popMStack

a12113b

Remove unused 'solve' function; makes no sense to have it in this PR,

8d95073

will bring it on the next one.

VictorCMiraldo mentioned this pull request Jun 15, 2022

In dev: Purify pirouette using a pure solve function, no more IO from the symbolic engine. #107

Closed

VictorCMiraldo merged commit 9970bd4 into dev Jun 15, 2022

VictorCMiraldo deleted the vcm/unsafePerformIO-smt-api branch June 15, 2022 07:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove explicit `IO` from our SMT interface #99

Remove explicit `IO` from our SMT interface #99

VictorCMiraldo commented May 29, 2022 •

edited

Loading

VictorCMiraldo commented Jun 14, 2022 •

edited

Loading

VictorCMiraldo commented Jun 14, 2022

0xd34df00d left a comment

0xd34df00d Jun 14, 2022

VictorCMiraldo Jun 15, 2022

serras Jun 15, 2022

VictorCMiraldo Jun 15, 2022

0xd34df00d Jun 14, 2022

VictorCMiraldo Jun 15, 2022

VictorCMiraldo Jun 15, 2022

serras commented Jun 15, 2022

VictorCMiraldo commented Jun 15, 2022 •

edited

Loading

VictorCMiraldo commented Jun 15, 2022

Remove explicit IO from our SMT interface #99

Remove explicit IO from our SMT interface #99

Conversation

VictorCMiraldo commented May 29, 2022 • edited Loading

What

Why

VictorCMiraldo commented Jun 14, 2022 • edited Loading

VictorCMiraldo commented Jun 14, 2022

0xd34df00d left a comment

Choose a reason for hiding this comment

0xd34df00d Jun 14, 2022

Choose a reason for hiding this comment

VictorCMiraldo Jun 15, 2022

Choose a reason for hiding this comment

serras Jun 15, 2022

Choose a reason for hiding this comment

VictorCMiraldo Jun 15, 2022

Choose a reason for hiding this comment

0xd34df00d Jun 14, 2022

Choose a reason for hiding this comment

VictorCMiraldo Jun 15, 2022

Choose a reason for hiding this comment

VictorCMiraldo Jun 15, 2022

Choose a reason for hiding this comment

serras commented Jun 15, 2022

VictorCMiraldo commented Jun 15, 2022 • edited Loading

VictorCMiraldo commented Jun 15, 2022

Remove explicit `IO` from our SMT interface #99

Remove explicit `IO` from our SMT interface #99

VictorCMiraldo commented May 29, 2022 •

edited

Loading

VictorCMiraldo commented Jun 14, 2022 •

edited

Loading

VictorCMiraldo commented Jun 15, 2022 •

edited

Loading