Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
inox
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LARA
inox
Commits
0b70ccac
Commit
0b70ccac
authored
10 years ago
by
Manos Koukoutos
Committed by
Etienne Kneuss
10 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Make CodeGenTests 7 times faster
parent
b453606d
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/test/scala/leon/test/codegen/CodeGenTests.scala
+326
-402
326 additions, 402 deletions
src/test/scala/leon/test/codegen/CodeGenTests.scala
with
326 additions
and
402 deletions
src/test/scala/leon/test/codegen/CodeGenTests.scala
+
326
−
402
View file @
0b70ccac
...
...
@@ -12,434 +12,358 @@ import EvaluationResults._
import
java.io._
case
class
TestCase
(
name
:
String
,
content
:
String
,
expected
:
Expr
,
args
:
Seq
[
Expr
]
=
Seq
(),
functionToTest
:
String
=
"test"
)
/*
* To add a new test:
* - Add your test, preferably in a new module, in the test variable
* - Make sure the function under test is named "test" and has no parameters
* - Add the test name and expected result in the result variable.
* Make sure the relative order of the tests matches that of code
*/
class
CodeGenTests
extends
test
.
LeonTestSuite
{
val
catchAll
=
true
val
pipeline
=
utils
.
TemporaryInputPhase
andThen
frontends
.
scalac
.
ExtractionPhase
andThen
utils
.
PreprocessingPhase
def
compileTestFun
(
p
:
Program
,
toTest
:
String
,
ctx
:
LeonContext
,
requireMonitor
:
Boolean
,
doInstrument
:
Boolean
)
:
(
Seq
[
Expr
]
=>
EvaluationResults
.
Result
)
=
{
// We want to produce code that checks contracts
val
evaluator
=
new
CodeGenEvaluator
(
ctx
,
p
,
CodeGenParams
(
maxFunctionInvocations
=
if
(
requireMonitor
)
1000
else
-
1
,
// Monitor calls and abort execution if more than X calls
checkContracts
=
true
,
// Generate calls that checks pre/postconditions
doInstrument
=
doInstrument
// Instrument reads to case classes (mainly for vanuatoo)
))
val
testFun
=
p
.
definedFunctions
.
find
(
_
.
id
.
name
==
toTest
).
getOrElse
{
ctx
.
reporter
.
fatalError
(
"Test function not defined!"
)
}
val
params
=
testFun
.
params
map
{
_
.
id
}
val
body
=
testFun
.
body
.
get
// Will apply test a number of times with the help of compileRec
evaluator
.
compile
(
body
,
params
).
getOrElse
{
ctx
.
reporter
.
fatalError
(
"Failed to compile test function!"
)
}
}
case
class
TestCase
(
name
:
String
,
expectedResult
:
Expr
,
testFunction
:
FunDef
)
def
runTests
()
=
{
val
catchAll
=
true
private
def
testCodeGen
(
prog
:
TestCase
,
requireMonitor
:
Boolean
,
doInstrument
:
Boolean
)
{
test
(
prog
.
name
)
{
import
prog._
val
pipeline
=
utils
.
TemporaryInputPhase
andThen
frontends
.
scalac
.
ExtractionPhase
andThen
utils
.
PreprocessingPhase
val
ctx
=
createLeonContext
()
val
ast
=
pipeline
.
run
(
ctx
)(
(
code
,
List
())
)
val
ast
=
pipeline
.
run
(
ctx
)(
(
content
,
List
())
)
val
testFuns
=
ast
.
definedFunctions
.
filter
{
_
.
id
.
name
==
"test"
}.
sortWith
{
(
f1
,
f2
)
=>
f1
.
getPos
<
f2
.
getPos
}
val
compiled
=
compileTestFun
(
ast
,
functionToTest
,
ctx
,
requireMonitor
,
doInstrument
)
try
{
compiled
(
args
)
match
{
case
Successful
(
res
)
if
res
==
expected
=>
// Success
case
RuntimeError
(
_
)
|
EvaluatorError
(
_
)
if
expected
.
isInstanceOf
[
Error
]
=>
// Success
case
Successful
(
res
)
=>
ctx
.
reporter
.
fatalError
(
s
"""
Program $name produced wrong output.
Output was ${res.toString}
Expected was ${expected.toString}
"""
.
stripMargin
)
case
RuntimeError
(
mes
)
=>
ctx
.
reporter
.
fatalError
(
s
"Program $name threw runtime error with message $mes"
)
case
EvaluatorError
(
res
)
=>
ctx
.
reporter
.
fatalError
(
s
"Evaluator failed for program $name with message $res"
)
}}
catch
{
// Currently, this is what we would like to catch and still succeed, but there might be more
case
_
:
LeonFatalError
|
_
:
StackOverflowError
if
expected.isInstanceOf
[
Error
]
=>
// Success
case
th
:
Throwable
=>
if
(
catchAll
)
{
// This is to be able to continue testing after an error
ctx
.
reporter
.
fatalError
(
s
"Program $name failed\n${th.printStackTrace()}"
)
// with message ${th.getMessage()}")
}
else
{
throw
th
}
val
testCases
=
results
zip
testFuns
map
{
case
(
(
name
,
result
),
fd
)
=>
TestCase
(
name
,
result
,
fd
)
}
}}
val
programs
=
Seq
(
TestCase
(
"simple"
,
"""
object simple {
abstract class Abs
case class Conc(x : Int) extends Abs
def test = {
val c = Conc(1)
c.x
}
}"""
,
IntLiteral
(
1
)
),
assert
(
results
.
size
==
testFuns
.
size
)
TestCase
(
"simpleBigInt"
,
"""
object simple {
abstract class Abs
case class Conc(x : BigInt) extends Abs
def test = {
val c = Conc(1)
c.x
}
}"""
,
InfiniteIntegerLiteral
(
1
)
),
TestCase
(
"eager"
,
"""
object eager {
abstract class Abs() {
val foo = 42
}
case class Conc(x : Int) extends Abs()
def foo = {
val c = Conc(1)
c.foo + c.x
}
def test = foo
}"""
,
IntLiteral
(
43
)
),
TestCase
(
"this"
,
"""
object thiss {
case class Bar() {
def boo = this
def toRet = 42
}
def test = Bar().boo.toRet
for
{
requireMonitor
<-
Seq
(
false
,
true
)
doInstrument
<-
Seq
(
false
,
true
)
evaluator
=
new
CodeGenEvaluator
(
createLeonContext
(),
ast
,
CodeGenParams
(
maxFunctionInvocations
=
if
(
requireMonitor
)
1000
else
-
1
,
// Monitor calls and abort execution if more than X calls
checkContracts
=
true
,
// Generate calls that checks pre/postconditions
doInstrument
=
doInstrument
// Instrument reads to case classes (mainly for vanuatoo)
))
TestCase
(
name
,
expected
,
testFunction
)
<-
testCases
suffix
=
(
if
(
requireMonitor
)
"M"
else
""
)
+
(
if
(
doInstrument
)
"I"
else
""
)
}
test
(
name
+
suffix
)
{
val
body
=
testFunction
.
body
.
get
val
params
=
testFunction
.
params
map
{
_
.
id
}
val
compiled
=
evaluator
.
compile
(
body
,
params
).
getOrElse
{
ctx
.
reporter
.
fatalError
(
"Failed to compile test function!"
)
}
"""
,
IntLiteral
(
42
)
),
TestCase
(
"oldStuff"
,
"""
object oldStuff {
def test = 1
case class Bar() {
def boo = 2
}
}"""
,
IntLiteral
(
1
)
),
TestCase
(
"methSimple"
,
"""
object methSimple {
sealed abstract class Ab {
def f2(x : Int) = x + 5
}
case class Con() extends Ab { }
def test = Con().f2(5)
}"""
,
IntLiteral
(
10
)
),
try
{
compiled
(
Nil
)
match
{
case
Successful
(
res
)
if
res
==
expected
=>
// Success
case
RuntimeError
(
_
)
|
EvaluatorError
(
_
)
if
expected
.
isInstanceOf
[
Error
]
=>
// Success
case
Successful
(
res
)
=>
ctx
.
reporter
.
fatalError
(
s
"""
Program $name produced wrong output.
Output was ${res.toString}
Expected was ${expected.toString}
"""
.
stripMargin
)
case
RuntimeError
(
mes
)
=>
ctx
.
reporter
.
fatalError
(
s
"Program $name threw runtime error with message $mes"
)
case
EvaluatorError
(
res
)
=>
ctx
.
reporter
.
fatalError
(
s
"Evaluator failed for program $name with message $res"
)
}}
catch
{
// Currently, this is what we would like to catch and still succeed, but there might be more
case
_
:
LeonFatalError
|
_
:
StackOverflowError
if
expected.isInstanceOf
[
Error
]
=>
// Success
case
th
:
Throwable
=>
if
(
catchAll
)
{
// This is to be able to continue testing after an error
println
(
s
"Program $name failed!"
)
th
.
printStackTrace
()
ctx
.
reporter
.
fatalError
(
s
"Program $name failed\n${th.printStackTrace()}"
)
// with message ${th.getMessage()}")
}
else
{
throw
th
}
}
}
}
TestCase
(
"methMakeBigInt"
,
"""
object methSimple {
val x: BigInt = 42
val
results
=
Seq
(
(
"simple"
,
IntLiteral
(
1
)),
(
"simpleBigInt"
,
InfiniteIntegerLiteral
(
1
)),
(
"eager"
,
IntLiteral
(
43
)),
(
"this"
,
IntLiteral
(
42
)
),
(
"oldStuff"
,
IntLiteral
(
1
)),
(
"methSimple"
,
IntLiteral
(
10
)),
(
"methMakeBigInt"
,
InfiniteIntegerLiteral
(
42
)),
(
"methSimpleBigInt"
,
InfiniteIntegerLiteral
(
10
)),
(
"BigIntNoOverflow"
,
InfiniteIntegerLiteral
(
BigInt
(
"4000000000"
))),
(
"BigIntOps"
,
InfiniteIntegerLiteral
(
BigInt
(
7
))),
(
"BigIntComp0"
,
BooleanLiteral
(
true
)),
(
"BigIntComp1"
,
InfiniteIntegerLiteral
(
BigInt
(
17
))),
(
"BigIntComp2"
,
InfiniteIntegerLiteral
(
BigInt
(
12
))),
(
"BigIntComp3"
,
InfiniteIntegerLiteral
(
BigInt
(-
7
))),
(
"methods"
,
IntLiteral
(
15
)),
(
"lazy"
,
IntLiteral
(
1
+
5
+
1
+
6
+
2
)
),
(
"modules"
,
IntLiteral
(
1
+
2
+
0
)
),
(
"lazyISLazy"
,
IntLiteral
(
42
)
),
(
"ListWithSize"
,
IntLiteral
(
3
)
),
(
"ListWithSumMono"
,
IntLiteral
(
1
+
2
+
3
)
),
(
"poly"
,
IntLiteral
(
42
)
),
(
"ListHead"
,
IntLiteral
(
1
)),
(
"ListWithSum"
,
IntLiteral
(
1
+
2
+
3
)
),
// This one loops!
(
"lazyLoops"
,
Error
(
Untyped
,
"Looping"
)
),
(
"Lazier"
,
IntLiteral
(
1
+
2
+
3
)
),
(
"SetToList"
,
BooleanLiteral
(
true
)
)
)
def test = x
}"""
,
InfiniteIntegerLiteral
(
42
)
),
TestCase
(
"methSimpleBigInt"
,
"""
object methSimple {
sealed abstract class Ab {
def f2(x : BigInt): BigInt = x + 5
}
case class Con() extends Ab { }
def test = Con().f2(5)
}"""
,
InfiniteIntegerLiteral
(
10
)
),
TestCase
(
"BigIntNoOverflow"
,
"""
object methSimple {
sealed abstract class Ab {
def f2(x : BigInt): BigInt = x + BigInt(2000000000)
}
case class Con() extends Ab { }
def test = Con().f2(2000000000)
}"""
,
InfiniteIntegerLiteral
(
BigInt
(
"4000000000"
))
),
val
code
=
"""
TestCase
(
"BigIntOps"
,
"""
object methSimple {
object simple {
abstract class Abs
case class Conc(x : Int) extends Abs
def test = {
val c = Conc(1)
c.x
def f(x: BigInt): BigInt = ((x * 2) - 10)/2
}
}
object simple2 {
abstract class Abs
case class Conc(x : BigInt) extends Abs
def test = {
val c = Conc(1)
c.x
def test = f(12)
}"""
,
InfiniteIntegerLiteral
(
BigInt
(
7
))
),
}
}
object eager {
abstract class Abs() {
val foo = 42
}
case class Conc(x : Int) extends Abs()
def foo = {
val c = Conc(1)
c.foo + c.x
}
def test = foo
}
object thiss {
case class Bar() {
def boo = this
def toRet = 42
}
def test = Bar().boo.toRet
}
object oldStuff {
def test = 1
case class Bar() {
def boo = 2
}
}
object methSimple {
sealed abstract class Ab {
def f2(x : Int) = x + 5
}
case class Con() extends Ab { }
def test = Con().f2(5)
}
object methSimple2 {
val x: BigInt = 42
def test = x
TestCase
(
"BigIntComp0"
,
"""
object methSimple {
def f(x: BigInt): Boolean = x == BigInt(17)
def test = f(17)
}"""
,
BooleanLiteral
(
true
)
),
TestCase
(
"BigIntComp1"
,
"""
object methSimple {
def f(x: BigInt): BigInt = if(x <= 0) -x else x
def test = f(-17)
}"""
,
InfiniteIntegerLiteral
(
BigInt
(
17
))
),
TestCase
(
"BigIntComp2"
,
"""
object methSimple {
def f(x: BigInt): BigInt = if(x < 0) -x else x
def test = f(-12)
}"""
,
InfiniteIntegerLiteral
(
BigInt
(
12
))
),
TestCase
(
"BigIntComp3"
,
"""
object methSimple {
def f(x: BigInt): BigInt = if(x >= 0) -x else x
def test = f(-7)
}"""
,
InfiniteIntegerLiteral
(
BigInt
(-
7
))
),
TestCase
(
"methods"
,
"""
object methods {
def f1 = 4
sealed abstract class Ab {
def f2(x : Int) = Cs().f3(1,2) + f1 + x + 5
}
case class Con() extends Ab {}
case class Cs() {
def f3(x : Int, y : Int) = x + y
}
def test = Con().f2(3)
}"""
,
IntLiteral
(
15
)
),
TestCase
(
"lazy"
,
"""
object lazyFields {
def foo = 1
sealed abstract class Ab {
lazy val x : Int = this match {
case Conc(t) => t + 1
case Conc2(t) => t+2
}
}
case class Conc(t : Int) extends Ab { }
case class Conc2(t : Int) extends Ab { }
def test = foo + Conc(5).x + Conc2(6).x
}
object methSimple3 {
sealed abstract class Ab {
def f2(x : BigInt): BigInt = x + 5
}
"""
,
IntLiteral
(
1
+
5
+
1
+
6
+
2
)
),
TestCase
(
"modules"
,
"""
object modules {
def foo = 1
val bar = 2
lazy val baz = 0
def test = foo + bar + baz
case class Con() extends Ab { }
def test = Con().f2(5)
}
object methSimple4 {
sealed abstract class Ab {
def f2(x : BigInt): BigInt = x + BigInt(2000000000)
}
"""
,
IntLiteral
(
1
+
2
+
0
)
),
TestCase
(
"lazyISLazy"
,
"""
object lazyISLazy {
abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
case class Conc() extends Ab { }
def test = { val willNotLoop = Conc(); 42 }
}"""
,
IntLiteral
(
42
)
),
TestCase
(
"ListWithSize"
,
"""
object list {
abstract class List[T] {
val length : Int = this match {
case Nil() => 0
case Cons (_, xs ) => 1 + xs.length
}
}
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = l.length + Nil().length
}"""
,
IntLiteral
(
3
)
),
TestCase
(
"ListWithSumMono"
,
"""
object ListWithSumMono {
abstract class List
case class Cons(hd : Int, tl : List) extends List
case class Nil() extends List
def sum (l : List) : Int = l match {
case Nil() => 0
case Cons(x, xs) => x + sum(xs)
case class Con() extends Ab { }
def test = Con().f2(2000000000)
}
object methSimple5 {
def f(x: BigInt): BigInt = ((x * 2) - 10)/2
def test = f(12)
}
object methSimple6 {
def f(x: BigInt): Boolean = x == BigInt(17)
def test = f(17)
}
object methSimple7 {
def f(x: BigInt): BigInt = if(x <= 0) -x else x
def test = f(-17)
}
object methSimple8 {
def f(x: BigInt): BigInt = if(x < 0) -x else x
def test = f(-12)
}
object methSimple9 {
def f(x: BigInt): BigInt = if(x >= 0) -x else x
def test = f(-7)
}
object methods {
def f1 = 4
sealed abstract class Ab {
def f2(x : Int) = Cs().f3(1,2) + f1 + x + 5
}
case class Con() extends Ab {}
case class Cs() {
def f3(x : Int, y : Int) = x + y
}
def test = Con().f2(3)
}
object lazyFields {
def foo = 1
sealed abstract class Ab {
lazy val x : Int = this match {
case Conc(t) => t + 1
case Conc2(t) => t+2
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}"""
,
IntLiteral
(
1
+
2
+
3
)
),
TestCase
(
"poly"
,
"""
object poly {
case class Poly[T](poly : T)
def ex = Poly(42)
def test = ex.poly
}"""
,
IntLiteral
(
42
)
),
TestCase
(
"ListHead"
,
"""
object ListHead {
abstract class List[T]
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def l = Cons(1, Cons(2, Cons(3, Nil())))
def test = l.hd
}"""
,
IntLiteral
(
1
)
),
TestCase
(
"ListWithSum"
,
"""
object ListWithSum {
abstract class List[T]
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def sum (l : List[Int]) : Int = l match {
}
case class Conc(t : Int) extends Ab { }
case class Conc2(t : Int) extends Ab { }
def test = foo + Conc(5).x + Conc2(6).x
}
object modules {
def foo = 1
val bar = 2
lazy val baz = 0
def test = foo + bar + baz
}
object lazyISLazy {
abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
case class Conc() extends Ab { }
def test = { val willNotLoop = Conc(); 42 }
}
object list {
abstract class List[T] {
val length : Int = this match {
case Nil() => 0
case Cons
(x
, xs) =>
x
+
sum(xs)
case Cons
(_
, xs
) =>
1
+
xs.length
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}"""
,
IntLiteral
(
1
+
2
+
3
)
),
// This one loops!
TestCase
(
"lazyLoops"
,
"""
object lazyLoops {
abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
case class Conc() extends Ab { }
def test = Conc().x
}"""
,
Error
(
Untyped
,
"Looping"
)
),
TestCase
(
"Lazier"
,
"""
}
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = l.length + Nil().length
}
object ListWithSumMono {
abstract class List
case class Cons(hd : Int, tl : List) extends List
case class Nil() extends List
def sum (l : List) : Int = l match {
case Nil() => 0
case Cons(x, xs) => x + sum(xs)
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}
object poly {
case class Poly[T](poly : T)
def ex = Poly(42)
def test = ex.poly
}
object ListHead {
abstract class List[T]
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def l = Cons(1, Cons(2, Cons(3, Nil())))
def test = l.hd
}
object ListWithSum {
abstract class List[T]
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def sum (l : List[Int]) : Int = l match {
case Nil() => 0
case Cons(x, xs) => x + sum(xs)
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}
object lazyLoops {
abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
case class Conc() extends Ab { }
def test = Conc().x
}
object Lazier {
import leon.lang._
object Lazier {
abstract class List[T] {
lazy val tail = this match {
case Nil() => error[List[T]]("Nil.tail")
case Cons(_, tl) => tl
}
abstract class List[T] {
lazy val tail = this match {
case Nil() => error[List[T]]("Nil.tail")
case Cons(_, tl) => tl
}
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def sum (l : List[Int]) : Int = l match {
case Nil() => 0
case c : Cons[Int] => c.hd + sum(c.tail)
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}"""
,
IntLiteral
(
1
+
2
+
3
)
),
TestCase
(
"SetToList"
,
"""
}
case class Cons[T](hd : T, tl : List[T]) extends List[T]
case class Nil[T]() extends List[T]
def sum (l : List[Int]) : Int = l match {
case Nil() => 0
case c : Cons[Int] => c.hd + sum(c.tail)
}
val l = Cons(1, Cons(2, Cons(3, Nil())))
def test = sum(l)
}
object SetToList {
import leon.collection._
object SetToList {
def test = {
val s = Set(1, 2, 3, 4, 5)
val s2 = setToList(s).content
s == s2
}
}"""
,
BooleanLiteral
(
true
)
)
)
for
(
prog
<-
programs
;
requireMonitor
<-
Seq
(
false
,
true
);
doInstrument
<-
Seq
(
false
,
true
)
)
{
testCodeGen
(
prog
.
copy
(
name
=
prog
.
name
+
(
if
(
requireMonitor
)
"_M_"
else
""
)
+
(
if
(
doInstrument
)
"_I_"
else
""
)),
requireMonitor
,
doInstrument
)}
def test = {
val s = Set(1, 2, 3, 4, 5)
val s2 = setToList(s).content
s == s2
}
}
"""
runTests
()
}
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment