billhallahan / g2 Goto Github PK

View Code? Open in Web Editor NEW

32.0 32.0 6.0 59.19 MB

License: Other

Haskell 76.20% Shell 0.03% Python 1.90% SMT 21.87%

haskell symbolic-execution

g2's People

Contributors

Stargazers

Watchers

Forkers

santolucito mrushyendra 2jacobtan rtlevy jhln binghamton-university-cs

g2's Issues

Liquid flag (--liquid & --liquid-func)

Hey hey,

I had some problems running the tool with cabal.. When running with stack it works if the following extra dependency is added:

optparse-applicative-0.17.0.0@sha256:0713e54cbb341e5cae979e2ac441eb3a5ff42e303001f432bd58c19e5638bdda,4967

While following the instructions from the readme file, the "Reachability" example works. But the LiquidHaskell example fails by saying that "--liquid" is not a valid flag.
I would like to ask if this is a functionality that was removed or if I am doing something wrong

Prim2 remI1 Test

The function remI1 defined in tests/Prim/Prim2.hs does not behave correctly on all inputs: the expression "remI1 (-9) (-8)" should evaluate to False, but it evaluates to True instead.

Unexpected results with integer division

Take the following function and symbolically evaluates in G2 with --n 1200 reduction steps.

foo :: Integer -> Bool
foo x = (div x 2) > 1

G2 generates a few concrete values for branches leading to True including 2 or 3 which do not check the predicate foo.

Symbolic Link Table

Implement a symbolic link table for tracing renaming.

add support for ghc > 8.2.2

Import statements should work

Currently, we cannot handle files that include import statements, we need to figure out how to deal with these.

Higher order functions, uninterpreted

It should be possible to find input to a higher order function that makes use of an uninterpreted function.

QuasiQuote de Bruijn benchmarks failed with 'Unrecognized Data' Error

Hi! I am trying to reproduce the results in your G2Q paper, and I tried to run

cabal run QuasiQuote

The other three set of benchmarks worked smoothly, while the de Bruijn benchmark failed with the following out. Could you please help me check what was happening? I am using GHC 8.10.7.

-- DeBruijn Eval -------
QuasiQuote: Unrecognized Data (DataCon (Name ":" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE))) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE))))))) with args [Type (TyCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) TYPE),App (App (App (App (Data (DataCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE)) (TyForAll (NamedTyBndr (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE)) (TyApp (TyApp (TyCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) (TyFun TYPE (TyFun TYPE TYPE))) (TyVar (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE))) (TyVar (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE))))))))) (Type (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) TYPE))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))) (App (App (App (Data (DataCon (Name ":" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE))) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 1)))))))) (App (Data (DataCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 1))))))),App (App (App (Data (DataCon (Name ":" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE))) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))))) (Type (TyCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) TYPE))) (App (App (App (App (Data (DataCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE)) (TyForAll (NamedTyBndr (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE)) (TyApp (TyApp (TyCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) (TyFun TYPE (TyFun TYPE TYPE))) (TyVar (Id (Name "a" (Just "GHC.Tuple") 0 Nothing) TYPE))) (TyVar (Id (Name "a" (Just "GHC.Tuple") 1 Nothing) TYPE))))))))) (Type (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) TYPE))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))) (App (App (App (Data (DataCon (Name ":" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyFun (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE))) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 1))))))))) (App (Data (DataCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))) (Type (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "Lam" (Just "DeBruijn.Interpreter") 8214565720327906922 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (App (Data (DataCon (Name "App" (Just "DeBruijn.Interpreter") 8214565720327906923 Nothing) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyFun (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 2))))) (App (Data (DataCon (Name "Var" (Just "DeBruijn.Interpreter") 8214565720327906921 Nothing) (TyFun (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE) (TyCon (Name "Expr" (Just "DeBruijn.Interpreter") 8214565720327906920 Nothing) TYPE)))) (App (Data (DataCon (Name "I#" (Just "GHC.Types") 8214565720327925190 Nothing) (TyFun TyLitInt (TyCon (Name "Int" (Just "GHC.Types") 8214565720327925189 Nothing) TYPE)))) (Lit (LitInt 1)))))))))) (App (Data (DataCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 0 Nothing) TYPE)) (TyApp (TyCon (Name "[]" (Just "GHC.Types") 0 Nothing) (TyFun TYPE TYPE)) (TyVar (Id (Name "a" Nothing 0 Nothing) TYPE)))))) (Type (TyCon (Name "(,)" (Just "GHC.Tuple") 0 Nothing) TYPE)))] in funcToSMT
CallStack (from HasCallStack):
  error, called at src/G2/Solver/Converters.hs:365:17 in g2-0.1.0.1-inplace:G2.Solver.Converters

Pipeline of commands.

Enable end user of G2 to quickly perform symbolic execution by supplying an easy pipeline of something like Interface.go functions.

e.g.:

main = do
    ...
    g2_core    <- Translator.Interface.go        filename
    prep_core  <- Preprocessing.Interface.go     g2_core
    sym_states <- SymbolicExecution.Interface.go pp_core
    solved     <- SMT.Interface.go               sym_states
    ....

Exact feeding of these Interface.go functions is to be determined, but this will dramatically lower the level of understanding that end users will actually have to understand about G2 internals in order to use it effectively.

Case statements in SMT

Case statements are currently not handled correctly in SMT formula. See preliminary SMT 2.6 Standard, pg 28, for correct handling:
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-draft-3.pdf

Error does not work properly with SMT conversion

When a function can throw an error, the SMT conversion does not process it correctly.

`irrefutPatError` with unsafe pattern matching in where clause

I have been running into some unexpected result with G2. I am not sure this is actually an issue or a subtlety I am not familiar with regarding non exhaustive pattern matching vs unsafe pattern matching in a where clause.

Consider the following functions:

foo :: Int -> Int
foo x = y
  where
    Just y = if x > 0 then Nothing else Just x

and

bar :: Int -> Int
bar x =
  case my of
    Just y -> y
  where
    my = if x > 0 then Nothing else Just x

There is a runtime execution when executing foo with G2 (irrefutPatError Irrefutable pattern failed for pattern)...

G2: evalVar: bad input.Id (Name "irrefutPatError" (Just "Control.Exception.Base") 3458764513820540937 Nothing) (TyForAll (NamedTyBndr (Id (Name "q" Nothing 3530822107858468881 Nothing) (TyCon (Name "RuntimeRep" (Just "GHC.Types") 3674937295934324926 Nothing) TYPE))) (TyForAll (NamedTyBndr (Id (Name "a" Nothing 3530822107858468865 Nothing) TYPE)) (TyFun (TyCon (Name "Addr#" (Just "GHC.Prim") 8214565720323796276 Nothing) TYPE) (TyVar (Id (Name "a" Nothing 3530822107858468865 Nothing) TYPE)))))
CallStack (from HasCallStack):
  error, called at src/G2/Execution/Rules.hs:124:19 in g2-0.1.0.1-inplace:G2.Execution.Rules

... whereas bar is executed normally and produces two branches including an error branch.

bar 0 = 0
bar 1 = error

Incorrect higher order counterexample from Nebula

On master, running:

time cabal run Nebula tests/RewriteVerify/Correct/TestZeno.hs p12

results in a generated (incorrect) counterexample:

--------------------
COUNTEREXAMPLE FOUND
--------------------
Left Path: Start -> a0 -> a4 -> a14
Right Path: Start -> b1 -> b5 -> b16
drop Z (map f'5 ((fs'4:fs'3))) = : _ (TICK[__ERROR_LABEL__'1]{error}) _ but map f'5 (drop Z ((fs'4:fs'3))) = : _ (TICK[__ERROR_LABEL__]{error}) _
Main Symbolic Variables:
f'5 = Symbolic T'3 -> T
xs = : @T'3 fs'4 fs'3
fs'4 = Symbolic T'3
fs'1 = TICK[__ERROR_LABEL__]{error}
fs = TICK[__ERROR_LABEL__'1]{error}
fs'3 = Symbolic ([] T'3)
a'112 = @T'1
f'5 = Symbolic T'3 -> T
n'21 = Z
a'110 = @T'2
Symbolic Function Mappings:
f'5 fs'4 --> fs'1
f'5 fs'4 --> fs
SAT ()

This appears to be caused by instType. If line 603 in G2.Interface.Interface:
https://github.com/BillHallahan/G2/blob/master/src/G2/Interface/Interface.hs#L603
is replaced with:

    let (ng'',exec_states') = (name_gen bindings', exec_states) -- L.mapAccumL instType (name_gen bindings') exec_states

Nebula is able to (correctly) prove the property.

Let expression bindings are not properly handled in Translator.hs

I don't think that LetRec expressions can be handled by a fold since the nature of the mutually recursive bindings induces an infinite loop.

SLT for Apply types

We need an SLT for tracking Apply types/constructors -> functions, that is distinct from the SLT for fresh variables.

Unsoundness from PrimReplace

If a user hides the Prelude definition of a function handled by PrimReplace, PrimReplace will replace that function anyway.

Formatting for output

Format the output to be easily readable.
Models from SMT solver should be parsed back into Core2.

Add support for preconditions

We currently have support to look for inputs that lead to a particular post condition. We need to be able to specify similar predicates on the input, to establish preconditions. Ideally, able to support different combinations of arguments. I.e. if you have a function a -> b -> c, we want to be able to establish preconditions of the form a -> Bool or b -> Bool or a -> b -> Bool. Need to think about how to pass these instructions on command line.

Assume / Assert is slow

There is an approximately factor of 2 speed reduction when we condition with Assume instead of App. I have no idea why this happens because profiling with cabal based packages is a living nightmare.

Some interesting things to point out:

The test ran on my machine was 147 seconds vs 76 seconds, which is approximately a factor of 2 difference.
App (Lam b ...) exp bindings from App in initStateCond would theoretically immediately add (b, exp) into the environment. This is potentially bad if the binder is referred to multiple times within the Lam body because we cannot abuse graph reduction at the Core Haskell level.
The fact that there is a factor of 2 difference seems to suggest that the exp in the beginning is evaluated twice, redundantly.

Some possibilities include:

GHC compiles stepAssume / stepAssert in a way that somehow violates the appearance of graph reduction properties we were trying to make it do. If this were true, it would be truly ironic.
???

Slowdown from Package Loading

The change to checkRule in src/G2/Equiv/Verifier.hs that allows Nebula to load package dependencies also makes Nebula significantly slower when running on certain theorems. Some of the theorems with a noticeable slowdown are p55, p16finA, p24fin, p25fin, and p61fin.

Automatic Test Cases

Exactly what it sounds like.

Make a single allNames call in the beginning and keep track of it in the execution state.

allNames is a very important, but slow function that gives us a conflict list for free variables.

Recommend Projects

React

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

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

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

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
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.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

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

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.