Skip to content

Commit

Permalink
[ test, perf ] Add couple of kinda-performance tests
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Aug 28, 2024
1 parent 0516fad commit 82eaf40
Show file tree
Hide file tree
Showing 14 changed files with 393 additions and 0 deletions.
100 changes: 100 additions & 0 deletions examples/pil-fun/tests/gens/scala3-big/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
-------------------


@main
def cvzuetjiel(): Unit = {
if (5.+(0)).<(3 + (5 + 0)) then
val dmchetdx = () => {
def g(rgaqgckocj: Int, ncsohxrcub: Int, od: Int): Unit =
Console.println(1)
extension (v: Boolean)
def wvqqvju(dvhcgdu: Int, vrvf: Int) =
{}
def qxi(xbspfqp: Int, hrkngcq: Int, b: Boolean, jhthzccdm: Int, oxlgerrls: Boolean) =
def kmqoxhhpnh(fjkjth: Boolean, u: Boolean): Boolean = { true }
(hrkngcq + 5) + (hrkngcq + (6 + 1))
def k(hff: Int, n: Boolean, ezmtsapbn: Boolean, akf: Boolean, u: Int, fntcttc: Boolean, p: Boolean) = { }

g(3 + 3, 3.+(6.+(3)), (4.+(6)).+(2))
def kafenoj() = {
val pegnb: Int = 5 + (7 + (7 + 3))
extension (tekl: Boolean) def jbqlxo(nulqgumre: Int, hekazmm: Boolean, edjyaxj: Int, skwc: Boolean): Unit = { {} } : Unit

}
val m = (true && false) || (false.&&(5.<(3)))
var w = m
(7.+(2)) + 5
}
extension (ypsfwzjdbb: Boolean)
def zzhjkgasdx(lfaij: Boolean, vc: Boolean, fotskji: Boolean) = {
if ypsfwzjdbb then
val wy = 0 + dmchetdx()
if (6.+(wy)) == 1 then
val uadzbddybb = (5.+(dmchetdx())) + (dmchetdx() + wy)

else
val owqnwqh = 6

extension (nxeloqe: Boolean)
def gpgypic(zrjm: Boolean, txjfhtsy: Boolean): Unit =
{}

else
val ji = (7 < dmchetdx()).||((!(ypsfwzjdbb)).&&(4.<=(dmchetdx())))
if !(!(6.==(1))) then
val mn = (zabyz: Boolean, tuwuxa: Boolean, wurensoje: Int, sdgzni: Int, ve: Int) => { ve + (wurensoje + (wurensoje + wurensoje)) } : Int

else
if (1.+(0)).<=(dmchetdx().+(1 + dmchetdx())) then {

} else {

}

var kpbmnbyy: Boolean = false

var wgezrh: Int = 7
extension (fa: Boolean)
def llyvr(ijkncb: Boolean) = {
val wgxdtmngsl = (vc.&&(ypsfwzjdbb)).&&(false)
(wgezrh + 4) + 0
}
wgezrh = dmchetdx()

}
var ugniydjot: Boolean = (true && true) || (true || (false.||(false)))
if dmchetdx().<(dmchetdx().+(1)) then
var egcnugrbj = (dmchetdx().+(dmchetdx())) + 0
ugniydjot = false

else
if (dmchetdx().==(dmchetdx())).&&(ugniydjot) then
{}
else
{}
val aastn = (3 + 1).+(dmchetdx().+(1.+(dmchetdx())))

ugniydjot = dmchetdx().<=(1.+(2 + dmchetdx()))

else
Console.println((0 + 1).+(2.+(5)))
Console.println(2 + 5)
extension (dckmfvua: Boolean)
def jrdjrbte() = {
var qx: Int = 4
Console.println((qx.+(qx)) + 2)

}
((2 + 7).==(3.+(6))).jrdjrbte()
if false then {
((3 + 5).==(2 + 0)).jrdjrbte()

} else {
extension (yflaeiz: Int)
def nguyvcjy(wfjunn: Boolean, srdrrgctx: Int, owgqgsil: Int, rte: Int, ojxenpml: Boolean, ndhgxd: Boolean): Boolean =
(6.+(yflaeiz)).==(4 + (yflaeiz.+(4)))

}


}
6 changes: 6 additions & 0 deletions examples/pil-fun/tests/gens/scala3-big/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
rm -rf build

flock "$1" pack -q install-deps pil-fun && \
pack run pil-fun scala3 --seed 0,3 --tests 1 --model-fuel 7

rm -rf build
167 changes: 167 additions & 0 deletions examples/pil-fun/tests/gens/scala3-smaller/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,167 @@
-------------------


@main
def tvlt(): Unit = {
if (5.+(0)) < (2.+(2)) then {
var lybokfpr = (4.+(5)).+(4.+(5))
lybokfpr = lybokfpr
lybokfpr = 4.+(lybokfpr + 1)
lybokfpr = lybokfpr
var uo: Boolean = (lybokfpr + lybokfpr).==(3 + 0)

} else {
val qemiujv = (jjh: Int, gxdtmng: Int, zdkvk: Int, n: Int, zadrbgu: Boolean) => {
if (jjh + n) == zdkvk then
extension (cuohsl: Int)
def zmuqm(lnevjvz: Boolean, ssl: Int, ltiv: Int): Int = {
if (true.&&(true)).||(zadrbgu) then
if lnevjvz.&&(false && (!(zadrbgu))) then
{}

else
if (ltiv.==(zdkvk)) || (ssl.<(4)) then
{}
else
{}

(ssl.+(5)) + (n.+(6))
} : Int

else
extension (r: Int)
def mrew(nbasrya: Int, jqaak: Boolean, jpinulqg: Boolean, kazmm: Boolean) =
{}
def qsokaogqmr() = { }

val mbn = jjh.+(1)
val ltpicdael: Int = 6
var woyvgazf: Int = (4 + 0).+(6 + n)

} : Unit
if (3 == 1) && (0.==(4)) then
if (2 + 1).==(1 + 2) then
extension (r: Int) def naqxvjgxmb() = { 4 <= (r + 1) }
qemiujv(1, 6, 5.+(4), 4.+(0), (1.naqxvjgxmb()).||(false.||(true)))

else
if false then
{}
else
if true.||(false && false) then {

}

var wf: Boolean = (2.+(2)).<(2 + 2)

extension (xmfo: Boolean)
def qnog(jg: Boolean, tzmk: Int, ogkzgnyugn: Int, bzyegcnug: Int) = {
qemiujv(3, 0, 0, tzmk.+(6), 5 < (tzmk + 6))

}

else
var yqavod = false && true
qemiujv(6, 0, 0.+(4), 4.+(1), yqavod || (yqavod && yqavod))
val sxfdzhrrh = (zbdd: Boolean, acoykh: Boolean, cbde: Boolean, dngc: Boolean, bqf: Boolean, drzqpmieuq: Boolean) =>
{}

if false || (2 <= 4) then
val obaztbbz: Boolean = (1.+(2)).==(2 + 6)

else
val ji: Boolean = (2 + 4).==(0.+(1))
val xsjzzhjk = (rbjd: Boolean, msoanazo: Int, dbbygddcsy: Boolean, j: Int, ots: Boolean, axwjjdtw: Boolean) => { }


}
val jrqa: Boolean = !(false)
extension (yannoshffy: Int)
def kwc(qnbouij: Int, mtsapbnquq: Int): Unit =
var k: Boolean = true
k = !(!(!(jrqa)))

val llqkzrga = (deszncso: Boolean, dtwbodm: Boolean, wvqqvju: Boolean) => {
var x = (wvqqvju.&&(true)).||(4 == 5)
x = true
(6.+(3)).+(0.+(1))
}

}
-------------------

val kwyflaeizb = (0.+(5)).+(3.+(5))
val wfjunn = kwyflaeizb.+(kwyflaeizb + kwyflaeizb)
var lisrdrrgc: Int = 4.+(1)
val bh = (agieo: Boolean, qazggfrct: Int) =>
if (0.<=(3)) && (!(false)) then {
var fwiklya = lisrdrrgc

} else {
extension (psmyvssee: Int) def kmcysd(mc: Boolean, m: Int, kpwfobj: Int, g: Boolean, sk: Boolean) = { }

}
lisrdrrgc = (kwyflaeizb + qazggfrct).+(kwyflaeizb.+(5))
6
val qrnqnfy = (yovn: Boolean, t: Boolean) => {
if (true.||(yovn)) || yovn then {

}
yovn
}

@main
def chojxe(): Unit = {
if 1 < (kwyflaeizb.+(5)) then
{}
else
{}

}
-------------------

extension (xirzqm: Boolean)
def efqu(): Unit =
val tmxsbu = (5 == 6) && (!(false))
var xnzeyxyo: Boolean = 4 == (3 + 4)
extension (kg: Boolean)
def doxdnly() = {
if (1.+(5)).<=(5 + 4) then {
xnzeyxyo = true

}
if true then
{}
else
{}

}
var drjp: Boolean = (0 == 0).||(xirzqm && false)
if tmxsbu && (tmxsbu && false) then {

}

var cstczqacp = (0 + 3) == (5 + 5)

@main
def japky(): Unit = {
if cstczqacp then {
(4 < (0.+(1))).efqu()
extension (faco: Boolean)
def f(vunluob: Int, xgriaerel: Boolean, rhn: Boolean, ffmlvduuc: Boolean, l: Boolean): Unit = {
(5.==(vunluob)).efqu()

} : Unit
val tkhyrdnc = () => { (0.+(0)).==(3) } : Boolean

} else {
var gfknyi: Int = (1.+(3)) + (5.+(6))
var quusqeb = (4 + 4) + (gfknyi.+(2))
cstczqacp.efqu()

}
var cyopq: Int = (0 + 2) + (3 + 2)
cstczqacp = cstczqacp && (true.&&(cstczqacp))
val ycchap: Boolean = false

}
6 changes: 6 additions & 0 deletions examples/pil-fun/tests/gens/scala3-smaller/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
rm -rf build

flock "$1" pack -q install-deps pil-fun && \
pack run pil-fun scala3 --seed 0,3 --tests 3 --model-fuel 6

rm -rf build
28 changes: 28 additions & 0 deletions tests/derivation/core/big con 001/DerivedGen.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
module DerivedGen

import RunDerivedGen

import Deriving.Show

%default total

%language ElabReflection

record X where
constructor MkX
field1 : Nat
field2 : Nat
field3 : Nat
field4 : Nat
field5 : Nat
field6 : Nat
field7 : Nat
field8 : Nat

%hint ShowX : Show X; ShowX = %runElab derive

checkedGen : Fuel -> Gen MaybeEmpty X
checkedGen = deriveGen

main : IO ()
main = runGs [ G checkedGen ]
1 change: 1 addition & 0 deletions tests/derivation/core/big con 001/RunDerivedGen.idr
1 change: 1 addition & 0 deletions tests/derivation/core/big con 001/derive.ipkg
24 changes: 24 additions & 0 deletions tests/derivation/core/big con 001/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
1/2: Building RunDerivedGen (RunDerivedGen.idr)
2/2: Building DerivedGen (DerivedGen.idr)
Generated values:
-----
-----
MkX 16 4 17 10 10 17 5 4
-----
MkX 12 11 8 15 4 14 7 4
-----
MkX 10 1 15 20 0 17 13 17
-----
MkX 17 12 2 18 13 10 14 16
-----
MkX 16 11 1 3 3 10 12 17
-----
MkX 19 7 3 16 6 12 18 2
-----
MkX 8 1 18 15 1 7 0 5
-----
MkX 15 19 3 19 9 6 4 0
-----
MkX 3 13 19 5 20 3 1 13
-----
MkX 9 5 0 7 4 7 6 16
1 change: 1 addition & 0 deletions tests/derivation/core/big con 001/run
32 changes: 32 additions & 0 deletions tests/derivation/core/big con 002/DerivedGen.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
module DerivedGen

import RunDerivedGen

import Deriving.Show

%default total

%language ElabReflection

record X where
constructor MkX
field0 : Nat
field1 : Nat
field2 : Nat
field3 : Nat
field4 : Nat
field5 : Nat
field6 : Nat
field7 : Nat
field8 : Nat
field9 : Nat
field10 : Nat
field11 : Nat

%hint ShowX : Show X; ShowX = %runElab derive

checkedGen : Fuel -> Gen MaybeEmpty X
checkedGen = deriveGen

main : IO ()
main = runGs [ G checkedGen ]
1 change: 1 addition & 0 deletions tests/derivation/core/big con 002/RunDerivedGen.idr
1 change: 1 addition & 0 deletions tests/derivation/core/big con 002/derive.ipkg
Loading

0 comments on commit 82eaf40

Please sign in to comment.