`stack test` crashes most of the time.

As I already stated during our meeting today, the testing library crashes approx. 9 / 10 times on my machine when I run stack test. It's possible that this is something weird that only happens on my machine. During the 9 times it crashes, it crashes on a different moment every time, and with different exceptions:

• Sometimes, weird exceptions that feel like C exceptions will be thrown (see 1, 2) and the ExitFailure is always -6 in those cases.
• The other times, no C memory exception will be showed and the ExitFailure is -11 (see 3).

Also, sometimes, the tests just all run correctly (see 0).

0

         Test Cases   Total       
 Passed  15           15          
 Failed  0            0           
 Total   15           15

1

$ stack test
> javawlp-0.1.0.0: test (suite: javawlp-tests)
> 
> EXAMPLES:
> ----PRE---- (swap_spec1 vs swap_spec2)
> e1:
> a != null && a.length > 0 && i >= 0 && j >= 0
> 
> e2:
> a != null && a[0] == 0 && a != null && a.length > 0 && i >= 0 && j > 0
> 
> LogicIR.Expr 1:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> LogicIR.Expr 2:
> LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LConst (CInt 0))) CEqual (LConst (CInt 0)))) LAnd (LBinop (LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGreater (LConst (CInt 0))))
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && int[]:a[0] == 0 && !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j > 0
> 
> ----PRE---- (test1 vs test2)
> e1:
> exists(a, i -> a[(i + 1)] > a[i])
> 
> e2:
> false
> 
> Z3 AST 1:
> (and (not a?null)
>      (bvsgt a?length #x00000000)
> LogicIR.Expr 1:
>      (bvsge i #x00000000)
> LQuant QAny (Var (TPrim PInt32) "i") (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CLess (LLen (Var (TArray (TPrim PInt32)) "a")))) (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LBinop (LVar (Var (TPrim PInt32) "i")) NAdd (LConst (CInt 1)))) CGreater (LArray (Var (TArray (TPrim PInt32)) "a") (LVar (Var (TPrim PInt32) "i"))))
>      (bvsge j #x00000000))
> ----PRE---- (getMax_spec1 vs getMax_spec2)
> 
> 
> LogicIR.Expr 2:
> LConst (CBool False)
> e1:
> 
> a != null && a.length > 0
> 
> e2:
> LogicIR.Pretty 1:
> a != null && a.length > 0
> Z3 AST 2:
> (QAny int:i: int:i >= 0 && int:i < len(int[]:a): int[]:a[int:i + 1] > int[]:a[int:i])
> 
> (and (not a?null)
> 
>      (= (select a #x00000000) #x00000000)
> LogicIR.Pretty 2:
> ----PRE---- (swap_spec1 vs swap_spec1)
>      (not a?null)
> false
> LogicIR.Expr 1:
>      (bvsgt a?length #x00000000)
> 
>      (bvsge i #x00000000)
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> e1:
>      (bvsgt j #x00000000))
> 
> a != null && a.length > 0 && i >= 0 && j >= 0
> 
> LogicIR.Expr 2:
> 
> e2:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> a != null && a.length > 0 && i >= 0 && j >= 0
> Z3 Result:
> 
> 
> LogicIR.Pretty 1:
> LogicIR.Expr 1:
> !isNull(int[]:a) && len(int[]:a) > 0
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> 
> LogicIR.Pretty 2:
> LogicIR.Expr 2:
> !isNull(int[]:a) && len(int[]:a) > 0
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> Z3 AST 1:
> (exists ((i (_ BitVec 32)))
>   (and (bvsge i #x00000000)
>        (bvslt i a?length)
>        (bvsgt (select a (bvadd i #x00000001)) (select a i))))
> 
> Z3 AST 2:
> false
> 
> Z3 Result:
> Z3 AST 1:
> (and (not a?null) (bvsgt a?length #x00000000))
> Z3 AST 1:
> 
> (and (not a?null)
>      (bvsgt a?length #x00000000)
>      (bvsge i #x00000000)
>      (bvsge j #x00000000))
> 
> Z3 AST 2:
> (and (not a?null) (bvsgt a?length #x00000000))
> 
> Z3 Result:
> Z3 AST 2:
> (and (not a?null)
>      (bvsgt a?length #x00000000)
>      (bvsge i #x00000000)
>      (bvsge j #x00000000))
> 
> Z3 Result:
> javawlp-tests(59221,0x70000ba4c000) malloc: *** error for object 0x7fac700056b0: pointer being freed was not allocated
> *** set a breakpoint in malloc_error_break to debug
> 
> Test suite failure for package javawlp-0.1.0.0
>     javawlp-tests:  exited with: ExitFailure (-6)
> Logs printed to consol

2

$ stack test
> javawlp-0.1.0.0: test (suite: javawlp-tests)
> 
> EXAMPLES:
> ----PRE---- (test1 vs test2)
> e1:
> exists(a, i -> a[(i + 1)] > a[i])
> 
> e2:
> false
> 
> LogicIR.Expr 1:
> ----PRE---- (getMax_spec1 vs getMax_spec2)
> LQuant QAny (Var (TPrim PInt32) "i") (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CLess (LLen (Var (TArray (TPrim PInt32)) "a")))) (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LBinop (LVar (Var (TPrim PInt32) "i")) NAdd (LConst (CInt 1)))) CGreater (LArray (Var (TArray (TPrim PInt32)) "a") (LVar (Var (TPrim PInt32) "i"))))
> 
> LogicIR.Expr 2:
> e1:
> LConst (CBool False)
> a != null && a.length > 0
> 
> 
> e2:
> a != null && a.length > 0
> LogicIR.Pretty 1:
> 
> (QAny int:i: int:i >= 0 && int:i < len(int[]:a): int[]:a[int:i + 1] > int[]:a[int:i])
> 
> LogicIR.Pretty 2:
> LogicIR.Expr 1:
> false
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> 
> 
> LogicIR.Expr 2:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && len(int[]:a) > 0
> 
> ----PRE---- (swap_spec1 vs swap_spec2)
> e1:
> a != null && a.length > 0 && i >= 0 && j >= 0
> 
> ----PRE---- (swap_spec1 vs swap_spec1)
> e2:
> e1:
> a != null && a[0] == 0 && a != null && a.length > 0 && i >= 0 && j > 0
> a != null && a.length > 0 && i >= 0 && j >= 0
> 
> 
> e2:
> a != null && a.length > 0 && i >= 0 && j >= 0
> LogicIR.Expr 1:
> 
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> LogicIR.Expr 2:
> LogicIR.Expr 1:
> LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LConst (CInt 0))) CEqual (LConst (CInt 0)))) LAnd (LBinop (LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGreater (LConst (CInt 0))))
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> 
> LogicIR.Expr 2:
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && int[]:a[0] == 0 && !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j > 0
> 
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> javawlp-tests(59235,0x70000534a000) malloc: *** error for object 0x7fa90ec02410: double free
> *** set a breakpoint in malloc_error_break to debug
> javawlp-tests(59235,0x700004fb5000) malloc: *** error for object 0x7fa90ec02410: double free
> *** set a breakpoint in malloc_error_break to debug
> javawlp-tests(59235,0x7000052c7000) malloc: *** error for object 0x7fa90ec02410: double free
> *** set a breakpoint in malloc_error_break to debug
> 
> Test suite failure for package javawlp-0.1.0.0
>     javawlp-tests:  exited with: ExitFailure (-6)
> Logs printed to console

3

$ stack test
> javawlp-0.1.0.0: test (suite: javawlp-tests)
> 
> EXAMPLES:
> ----PRE---- (test1 vs test2)
> e1:
> exists(a, i -> a[(i + 1)] > a[i])
> 
> e2:
> ----PRE---- (swap_spec1 vs swap_spec1)
> false
> 
> e1:
> a != null && a.length > 0 && i >= 0 && j >= 0
> LogicIR.Expr 1:
> 
> e2:
> a != null && a.length > 0 && i >= 0 && j >= 0
> LQuant QAny (Var (TPrim PInt32) "i") (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CLess (LLen (Var (TArray (TPrim PInt32)) "a")))) (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LBinop (LVar (Var (TPrim PInt32) "i")) NAdd (LConst (CInt 1)))) CGreater (LArray (Var (TArray (TPrim PInt32)) "a") (LVar (Var (TPrim PInt32) "i"))))
> 
> 
> LogicIR.Expr 2:
> LConst (CBool False)
> LogicIR.Expr 1:
> 
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> LogicIR.Expr 2:
> LogicIR.Pretty 1:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> (QAny int:i: int:i >= 0 && int:i < len(int[]:a): int[]:a[int:i + 1] > int[]:a[int:i])
> 
> LogicIR.Pretty 2:
> LogicIR.Pretty 1:
> false
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> 
> LogicIR.Pretty 2:
> ----PRE---- (getMax_spec1 vs getMax_spec2)
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> e1:
> a != null && a.length > 0
> 
> e2:
> a != null && a.length > 0
> 
> LogicIR.Expr 1:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> 
> LogicIR.Expr 2:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && len(int[]:a) > 0
> 
> ----PRE---- (swap_spec1 vs swap_spec2)
> e1:
> a != null && a.length > 0 && i >= 0 && j >= 0
> 
> e2:
> a != null && a[0] == 0 && a != null && a.length > 0 && i >= 0 && j > 0
> 
> LogicIR.Expr 1:
> LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0))) LAnd (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGeq (LConst (CInt 0)))))
> 
> LogicIR.Expr 2:
> LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LArray (Var (TArray (TPrim PInt32)) "a") (LConst (CInt 0))) CEqual (LConst (CInt 0)))) LAnd (LBinop (LBinop (LBinop (LUnop LNot (LIsnull (Var (TArray (TPrim PInt32)) "a"))) LAnd (LBinop (LLen (Var (TArray (TPrim PInt32)) "a")) CGreater (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CGeq (LConst (CInt 0)))) LAnd (LBinop (LVar (Var (TPrim PInt32) "j")) CGreater (LConst (CInt 0))))
> 
> LogicIR.Pretty 1:
> !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j >= 0
> 
> LogicIR.Pretty 2:
> !isNull(int[]:a) && int[]:a[0] == 0 && !isNull(int[]:a) && len(int[]:a) > 0 && int:i >= 0 && int:j > 0
> 
> 
> Test suite failure for package javawlp-0.1.0.0
>     javawlp-tests:  exited with: ExitFailure (-11)
> Logs printed to console

changed the description

Since the exceptions are weird C exceptions, my gut tells me that this is a problem Z3, possibly due to the fact that HUnit executes tests in parallel @o.melkonian?

Yep, definitely an issue with Z3:

• https://github.com/Z3Prover/z3/search?q=double+free&type=Issues&utf8=
• https://github.com/Z3Prover/z3/search?utf8=&q=pointer+being+freed+was+not+allocated&type=Issues

@j.s.tentusscher It seems to be an OSX-thing. Can you remove this line and check if the problem persists?

Solved by enforcing single-threaded execution of the test suite.

closed