billhallahan / g2 Goto Github PK
View Code? Open in Web Editor NEWLicense: Other
License: Other
Exactly what it sounds like.
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
.
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.
As I am testing the benchmark test cases with the inst-types function; I discovered this error G2: walkerFunc: bad argument passed. The test case where this error shows up is the myListId function that has the type myListId :: MyList a -> MyList a where MyList a is defined as
data MyList a where
Ni :: MyList a
Cons :: a -> MyList a -> MyList a
The error message read as follows
G2: walkerFunc: bad argument passed
[(Name "fs" Nothing 6989586621679063949 Nothing,Id (Name "fs" Nothing 6989586621679063950 Nothing) (TyFun (TyVar (Id (Name "fs" Nothing 6989586621679063949 Nothing) TYPE)) (TyVar (Id (Name "fs" Nothing 6989586621679063949 Nothing) TYPE))))]
TyVar (Id (Name "a" Nothing 6989586621679013373 (Just (Span {start = Loc {line = 49, col = 3, file = "/Users/qinghongwu/Downloads/G2/tests/TestFiles/InstTypes1.hs"}, end = Loc {line = 49, col = 36, file = "/Users/qinghongwu/Downloads/G2/tests/TestFiles/InstTypes1.hs"}}))) TYPE)
Furthermore, this issue pops up again when I am testing with types that take three type variables.
data Tri a b c where
Tri :: a -> b -> Maybe c -> Tri a b c
triId :: Tri a b c -> Tri a b c
triId x = x
G2: walkerFunc: bad argument passed
[(Name "fs" Nothing 6989586621679065524 Nothing,Id (Name "fs" Nothing 6989586621679065527 Nothing) (TyFun (TyVar (Id (Name "fs" Nothing 6989586621679065524 Nothing) TYPE)) (TyVar (Id (Name "fs" Nothing 6989586621679065524 Nothing) TYPE)))),(Name "fs" Nothing 6989586621679065523 Nothing,Id (Name "fs" Nothing 6989586621679065526 Nothing) (TyFun (TyVar (Id (Name "fs" Nothing 6989586621679065523 Nothing) TYPE)) (TyVar (Id (Name "fs" Nothing 6989586621679065523 Nothing) TYPE)))),(Name "fs" Nothing 6989586621679065522 Nothing,Id (Name "fs" Nothing 6989586621679065525 Nothing) (TyFun (TyVar (Id (Name "fs" Nothing 6989586621679065522 Nothing) TYPE)) (TyVar (Id (Name "fs" Nothing 6989586621679065522 Nothing) TYPE))))]
TyVar (Id (Name "c" Nothing 6989586621679014401 (Just (Span {start = Loc {line = 142, col = 3, file = "/Users/qinghongwu/Downloads/G2/tests/TestFiles/InstTypes1.hs"}, end = Loc {line = 142, col = 40, file = "/Users/qinghongwu/Downloads/G2/tests/TestFiles/InstTypes1.hs"}}))) TYPE)
CallStack (from HasCallStack):
I think this issue might be attributed to how we process the type variable in which we haven't processed every type variable required by the types.
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 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
Format the output to be easily readable.
Models from SMT solver should be parsed back into Core2.
Hey hey,
I had some problems running the tool with cabal.. When running with stack it works if the following extra dependency is added:
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
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.
Implement a symbolic link table for tracing renaming.
It should be possible to find input to a higher order function that makes use of an uninterpreted function.
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
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:
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.exp
in the beginning is evaluated twice, redundantly.Some possibilities include:
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.Currently, we cannot handle files that include import statements, we need to figure out how to deal with these.
The function in multiPrim tests/HigherOrder/HigherOrder.hs currently has an issue that might be attributed to the fact that we haven't covered the floating point number in the case expr in elimPrimDC from src/G2/Lib/Printers.hs
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.
allNames is a very important, but slow function that gives us a conflict list for free variables.
If a user hides the Prelude definition of a function handled by PrimReplace, PrimReplace will replace that function anyway.
When a function can throw an error, the SMT conversion does not process it correctly.
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
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.
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.
Now discovered that G2: WalkerFun is having an issue with GADT syntax specifically if we have
data MyList a where
Ni :: MyList a
Cons :: a -> MyList a -> MyList a
But if we have data MyList a = Ni | Cons a (MyList a) which is the same thing as above, G2 will work. Now we should consider how to make G2 understand and successfully process the GADT syntax
We need an SLT for tracking Apply types/constructors -> functions, that is distinct from the SLT for fresh variables.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.