Skip to content

Commit 62698d1

Browse files
committed
Merge remote-tracking branch 'origin/main' into scalatest-parallel
Conflicts: src/test/scala/SystemTests.scala
2 parents 30b0f1c + b45b98f commit 62698d1

File tree

73 files changed

+2720
-333
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

73 files changed

+2720
-333
lines changed
+33
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#!/bin/bash -eu
2+
3+
set -o pipefail
4+
5+
test_dir=src/test
6+
7+
echo '::group::All test suites:'
8+
tests="$(./mill test.testOnly -- -t '' -oW | tr -d ':' | sort)"
9+
echo "$tests"
10+
echo '::endgroup::'
11+
echo
12+
echo '::group::Disabled test suites:'
13+
grep --color=always '@test_util\.tags\.DisabledTest' --context=1 -R $test_dir
14+
echo '::endgroup::'
15+
echo
16+
17+
ok=true
18+
echo '::group::Test suites with no tag annotations:'
19+
for t in $tests; do
20+
defn="$(grep 'class\s\+'"$t"'[ (]' --before-context=2 -R $test_dir)"
21+
# search for lines which are entirely "@test_util.tags.*Test"
22+
# leading - is produced by grep to mark prefixes
23+
if ! grep -q -- '-@test_util\.tags\..\+Test$' <<< "$defn"; then
24+
echo 'test suite has no `@test_util.tags.*Test` annotation:' >&2
25+
grep --color=always 'class\s\+'"$t"'[ (]' --before-context=2 -R $test_dir
26+
echo
27+
ok=false
28+
fi
29+
done
30+
echo '::endgroup::'
31+
32+
$ok
33+

.github/workflows/run-examples.yml

+20-48
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,18 @@ on:
88
- main
99
workflow_dispatch:
1010
jobs:
11+
CheckTestTagging:
12+
runs-on: ubuntu-latest
13+
steps:
14+
- uses: actions/checkout@v4
15+
- uses: actions/setup-java@v4
16+
with:
17+
distribution: 'temurin'
18+
java-version: '21'
19+
- run: './mill test.compile'
20+
- name: Check all test suites have at least one tag
21+
run: .github/workflows/check-test-tagging.sh
22+
1123
Scalafmt:
1224
runs-on: ubuntu-latest
1325
steps:
@@ -52,8 +64,9 @@ jobs:
5264
- run: sudo apt-get install -y z3='4.8.12-*'
5365
- run: dotnet tool install --global boogie --version '3.4.3'
5466

55-
- name: System Tests
56-
run: ./mill test.testOnly 'SystemTests*'
67+
- run: ./mill compile
68+
- run: ./scripts/scalatest.sh -oID -n test_util.tags.StandardSystemTest
69+
5770
- uses: actions/upload-artifact@v4
5871
with:
5972
name: testresult-${{ github.run_number }}
@@ -103,44 +116,11 @@ jobs:
103116
- run: dotnet tool install --global boogie --version '3.4.3'
104117

105118
- run: ./mill test.compile
119+
- run: ./scripts/scalatest.sh -oID -n test_util.tags.UnitTest
106120

107121
# every test with package prefix:
108122
# sbt "show test:definedTests"
109123

110-
# note: tests prefixed with '!' are expected to fail.
111-
# if they are fixed, the '!' should be removed.
112-
113-
- run: ./mill test.testOnly IrreducibleLoop
114-
if: ${{ ! cancelled() }}
115-
- run: ./mill test.testOnly BitVectorAnalysisTests
116-
if: ${{ ! cancelled() }}
117-
- run: ./mill test.testOnly '*IntrusiveListPublicInterfaceTest'
118-
if: ${{ ! cancelled() }}
119-
- run: ./mill test.testOnly util.intrusive_list.IntrusiveListTest
120-
if: ${{ ! cancelled() }}
121-
- run: ./mill test.testOnly DataStructureAnalysisTest
122-
if: ${{ ! cancelled() }}
123-
- run: ./mill test.testOnly ParamAnalysisTests
124-
if: ${{ ! cancelled() }}
125-
- run: ./mill test.testOnly LiveVarsAnalysisTests
126-
if: ${{ ! cancelled() }}
127-
- run: ./mill test.testOnly ir.ToScalaTest
128-
if: ${{ ! cancelled() }}
129-
- run: ./mill test.testOnly ir.IRTest
130-
if: ${{ ! cancelled() }}
131-
- run: ./mill test.testOnly ir.IRToDSLTest
132-
if: ${{ ! cancelled() }}
133-
- run: ./mill test.testOnly ir.CILVisitorTest
134-
if: ${{ ! cancelled() }}
135-
- run: ./mill test.testOnly ir.InterpreterTests
136-
if: ${{ ! cancelled() }}
137-
- run: ./mill test.testOnly ir.InvariantTest
138-
if: ${{ ! cancelled() }}
139-
- run: ./mill test.testOnly ProcedureSummaryTests || true
140-
if: ${{ ! cancelled() }}
141-
- run: ./mill test.testOnly TaintAnalysisTests
142-
if: ${{ ! cancelled() }}
143-
144124
AnalysisSystemTests:
145125
runs-on: ubuntu-latest
146126

@@ -161,15 +141,7 @@ jobs:
161141
- run: sudo apt-get install -y z3='4.8.12-*'
162142
- run: dotnet tool install --global boogie --version '3.4.3'
163143

164-
- run: echo "All systemtest suites:" & ./mill test.testOnly '*SystemTests*' -- -z 'xxxx'
165-
166-
- run: ./mill test.testOnly DSAMemoryRegionSystemTestsBAP
167-
if: ${{ ! cancelled() }}
168-
- run: ./mill test.testOnly DSAMemoryRegionSystemTestsGTIRB
169-
if: ${{ ! cancelled() }}
170-
- run: ./mill test.testOnly AnalysisSystemTestsBAP
171-
if: ${{ ! cancelled() }}
172-
- run: ./mill test.testOnly AnalysisSystemTestsGTIRB
173-
if: ${{ ! cancelled() }}
174-
- run: ./mill test.testOnly SimplifySystemTests
175-
if: ${{ ! cancelled() }}
144+
- run: echo "All systemtest suites:" && ./mill test.testOnly '*SystemTests*' -- -z 'xxxx'
145+
146+
- run: ./mill compile
147+
- run: ./scripts/scalatest.sh -oID -n test_util.tags.AnalysisSystemTest

build.sc

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import contrib.scalapblib._
99
object basil extends RootModule with ScalaModule with antlr.AntlrModule with ScalaPBModule {
1010
def scalaVersion = "3.3.4"
1111

12-
// def scalacOptions: T[Seq[String]] = Seq("-Xprint:typer")
12+
def scalacOptions: T[Seq[String]] = Seq("-deprecation")
1313

1414
val javaTests = ivy"com.novocode:junit-interface:0.11"
1515
val scalaTests = ivy"org.scalatest::scalatest:3.2.19"

docs/development/testing.md

+148
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
Testing
2+
=======
3+
4+
Testing is crucial for validating new features and preventing regressions.
5+
It is important that tests are written for any new features, as well as any
6+
identified bugs.
7+
It is important that we should have a clear understanding of what each test
8+
is testing, whether it currently passes and, if not, why it is currently
9+
not working.
10+
This page will describe some tools in the codebase which help with developing
11+
and maintaining test cases.
12+
13+
Writing test cases
14+
------------------
15+
Test cases are written in Scalatest using its
16+
[`AnyFunSuite`](https://www.scalatest.org/scaladoc/3.1.2/org/scalatest/funsuite/AnyFunSuite.html) style.
17+
See the AnyFunSuite documentation or existing test cases for syntax and examples.
18+
19+
### Exporting IR structures into test cases
20+
21+
Often, you might have found a particular Basil IR program which demonstrates some bug in the code.
22+
It is good practice to extract this into a test case, both to validate the fix and ensure the bug doesn't reoccur.
23+
To help with this, a Basil IR program can be converted to
24+
a Scala literal by using the [ToScala](https://github.com/UQ-PAC/BASIL/blob/main/src/main/scala/ir/dsl/ToScala.scala)
25+
trait.
26+
27+
To do this, first `import ir.dsl.given`, then you can use the `.toScala` extension method on programs, procedures, or blocks.
28+
This gives you a string which is valid Scala code.
29+
This can be copied and pasted into a unit test.
30+
When executed, the Scala code to will re-construct that Basil IR structure using the DSL.
31+
32+
### Tagging test suites
33+
34+
[Tags](https://www.scalatest.org/scaladoc/3.2.1/org/scalatest/Tag.html)
35+
are used to categorise test classes based on, roughly, the kind of test (e.g., unit tests or system (end-to-end) tests).
36+
Each test suite should be tagged with one of the
37+
[`@test_util.tags.*Test`](https://github.com/UQ-PAC/BASIL/tree/main/src/test/scala/test_util/tags) tags,
38+
placed on the line before the AnyFunSuite class declaration.
39+
A test suite may, additionally, be tagged with one or more of the supplementary tags (those not ending in Test).
40+
41+
To run only tests from a specific tag, you can use
42+
```bash
43+
./scripts/scalatest.sh -o -n test_utils.tags.TagName
44+
```
45+
Note that the tag name must be fully-qualified (i.e., including the package name).
46+
See [the Scalatest runner docs](https://www.scalatest.org/user_guide/using_the_runner) or the `scalatest.sh` file
47+
for more options.
48+
49+
### Dynamic tests
50+
51+
Note that the `test("test name")` method can be written anywhere within a AnyFunSuite body, including
52+
within loops or conditionals.
53+
This allows you to dynamically generate test cases, as in
54+
Basil's [`SystemTests`](/src/test/scala/SystemTests.scala).
55+
This should be used sparingly.
56+
57+
58+
Maintaining test cases
59+
----------------------
60+
Over time, test cases might break due to code changes or refactoring.
61+
Of course, failing tests should be fixed as soon as possible.
62+
However, this is not always possible - maybe a test case relies on features not yet implemented.
63+
It might be reasonable to allow a test to fail for a period of time until the fixes are ready.
64+
In these cases, it is important that tests which are known/expected to fail are clearly marked
65+
and the reason for their failure should be recorded in the code.
66+
67+
Generally, the strategy is that failing tests should still be executed.
68+
They should be annotated so that they are allowed to fail, but if they start passing,
69+
that should raise an error until the annotation is removed.
70+
This allows the test code to be an accurate record of the expected outcome of each test.
71+
72+
73+
### pendingUntilFixed (for expected failures)
74+
75+
[`pendingUntilFixed`](https://www.scalatest.org/scaladoc/3.2.3/org/scalatest/Assertions.html#pendingUntilFixed(f:=%3EUnit)(implicitpos:org.scalactic.source.Position):org.scalatest.Assertionwithorg.scalatest.PendingStatement) should be used to mark a block of code (typically containing an assertion) as one which is currently expected to fail. This should be used to record test cases which fail due to not-yet-implemented features or known bugs. If a change is made and the code no longer fails, this will cause the test to fail until the pendingUntilFixed is removed.
76+
77+
It should be used within a `test() { ... }` block like so, with a comment documenting the cause of failure and expected future resolution.
78+
```scala
79+
test("1 == 2 sometime soon?") {
80+
assert(1 == 1, "obviously")
81+
82+
// broken until we fix maths
83+
pendingUntilFixed {
84+
assert(1 == 2, "todo")
85+
}
86+
}
87+
```
88+
89+
- Tests can be marked as ignored by replacing `test()` with `ignore()`. An entire suite can be marked as ignored with the `@org.scalatest.Ignore` annotation.
90+
91+
### TestCustomisation (for dynamically-generated tests)
92+
93+
For some tests, particularly those which are dynamically-generated by a loop, it is not practical to add a `pendingUntilFixed` block
94+
into the test body.
95+
For these cases, there is a `trait TestCustomisation` to help with customising dynamically-generated tests
96+
based on their test case name (for system tests, this includes the file path and compiler/lifter options).
97+
98+
To use this, the test suite class should be made to extend [TestCustomisation](/src/test/scala/test_util/TestCustomisation.scala).
99+
This defines an abstract method customiseTestsByName which controls the mode of each test case.
100+
```scala
101+
@test_util.tags.UnitTest
102+
class ProcedureSummaryTests extends AnyFunSuite, TestCustomisation {
103+
104+
override def customiseTestsByName(name: String) = {
105+
name match {
106+
case "test a" => Mode.NotImplemented("doesn't seem to work yet")
107+
case _ => Mode.Normal
108+
}
109+
}
110+
111+
test("test a") {
112+
assert(false);
113+
}
114+
115+
test("test b") {
116+
assert(true);
117+
}
118+
}
119+
```
120+
Test cases can be marked as retry, disabled, not implemented, or temporary failure
121+
(see TestCustomisation source file for more details).
122+
This modifies the behaviour of the test case and prints helpful output when running the test. For example:
123+
```c
124+
- correct/malloc_with_local3/clang:BAP (pending)
125+
+ NOTE: Test case is customised with: "ExpectFailure(previous failure was: Expected verification success, but got failure. Failing assertion is: assert (load37_1 == R30_in))"
126+
127+
+ Failing assertion ./src/test/correct/malloc_with_local3/clang/malloc_with_local3_bap.bpl:264
128+
+ 261 | load36_1, Gamma_load36_1 := memory_load64_le(mem_9, bvadd64(R31_in, 18446744073709551600bv64)), (gamma_load64(Gamma_mem_9, bvadd64(R31_in, 18446744073709551600bv64)) || L(bvadd64(R31_in, 18446744073709551600bv64)));
129+
262 | call rely();
130+
263 | load37_1, Gamma_load37_1 := memory_load64_le(mem_10, bvadd64(R31_in, 18446744073709551608bv64)), (gamma_load64(Gamma_mem_10, bvadd64(R31_in, 18446744073709551608bv64)) || L(bvadd64(R31_in, 18446744073709551608bv64)));
131+
> 264 | assert (load37_1 == R30_in); //is returning to caller-set R30
132+
265 | goto printCharValue_2260_basil_return;
133+
266 | printCharValue_2260_basil_return:
134+
267 | assume {:captureState "printCharValue_2260_basil_return"} true;
135+
```
136+
137+
```c
138+
- analysis_differential:malloc_with_local/gcc_O2:GTIRB (pending)
139+
+ NOTE: Test case is customised with: "ExpectFailure(needs printf_chk)"
140+
141+
+ STDOUT: ""
142+
```
143+
144+
Modes which expect failure (temp failure and not implemented) will show as "pending" when
145+
executing scalatest.
146+
The disabled mode will show as "cancelled".
147+
Both of these will be output in yellow text if your console is using colour.
148+

examples/sync_write_spinlock/sync_write.c

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ int secret;
77
int main() {
88
int expected = 0;
99
while (!atomic_compare_exchange_weak(&z, &expected, 1)) {
10+
expected = 0;
1011
while (z != 0) {
1112
}
1213
}
202 Bytes
Binary file not shown.

examples/sync_write_spinlock/sync_write.relf

+16-16
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,10 @@ Symbol table '.symtab' contains 92 entries:
4545
11: 0000000000000580 0 SECTION LOCAL DEFAULT 11 .init
4646
12: 00000000000005a0 0 SECTION LOCAL DEFAULT 12 .plt
4747
13: 0000000000000600 0 SECTION LOCAL DEFAULT 13 .text
48-
14: 00000000000007dc 0 SECTION LOCAL DEFAULT 14 .fini
49-
15: 00000000000007f0 0 SECTION LOCAL DEFAULT 15 .rodata
50-
16: 00000000000007f4 0 SECTION LOCAL DEFAULT 16 .eh_frame_hdr
51-
17: 0000000000000830 0 SECTION LOCAL DEFAULT 17 .eh_frame
48+
14: 00000000000007e0 0 SECTION LOCAL DEFAULT 14 .fini
49+
15: 00000000000007f4 0 SECTION LOCAL DEFAULT 15 .rodata
50+
16: 00000000000007f8 0 SECTION LOCAL DEFAULT 16 .eh_frame_hdr
51+
17: 0000000000000838 0 SECTION LOCAL DEFAULT 17 .eh_frame
5252
18: 0000000000010dc8 0 SECTION LOCAL DEFAULT 18 .init_array
5353
19: 0000000000010dd0 0 SECTION LOCAL DEFAULT 19 .fini_array
5454
20: 0000000000010dd8 0 SECTION LOCAL DEFAULT 20 .dynamic
@@ -61,16 +61,16 @@ Symbol table '.symtab' contains 92 entries:
6161
27: 0000000000000278 0 NOTYPE LOCAL DEFAULT 3 $d
6262
28: 0000000000000278 32 OBJECT LOCAL DEFAULT 3 __abi_tag
6363
29: 0000000000000600 0 NOTYPE LOCAL DEFAULT 13 $x
64-
30: 0000000000000844 0 NOTYPE LOCAL DEFAULT 17 $d
65-
31: 00000000000007f0 0 NOTYPE LOCAL DEFAULT 15 $d
64+
30: 000000000000084c 0 NOTYPE LOCAL DEFAULT 17 $d
65+
31: 00000000000007f4 0 NOTYPE LOCAL DEFAULT 15 $d
6666
32: 0000000000000000 0 FILE LOCAL DEFAULT ABS crti.o
6767
33: 0000000000000634 0 NOTYPE LOCAL DEFAULT 13 $x
6868
34: 0000000000000634 20 FUNC LOCAL DEFAULT 13 call_weak_fn
6969
35: 0000000000000580 0 NOTYPE LOCAL DEFAULT 11 $x
70-
36: 00000000000007dc 0 NOTYPE LOCAL DEFAULT 14 $x
70+
36: 00000000000007e0 0 NOTYPE LOCAL DEFAULT 14 $x
7171
37: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtn.o
7272
38: 0000000000000590 0 NOTYPE LOCAL DEFAULT 11 $x
73-
39: 00000000000007e8 0 NOTYPE LOCAL DEFAULT 14 $x
73+
39: 00000000000007ec 0 NOTYPE LOCAL DEFAULT 14 $x
7474
40: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
7575
41: 0000000000000650 0 NOTYPE LOCAL DEFAULT 13 $x
7676
42: 0000000000000650 0 FUNC LOCAL DEFAULT 13 deregister_tm_clones
@@ -83,19 +83,19 @@ Symbol table '.symtab' contains 92 entries:
8383
49: 0000000000000710 0 FUNC LOCAL DEFAULT 13 frame_dummy
8484
50: 0000000000010dc8 0 NOTYPE LOCAL DEFAULT 18 $d
8585
51: 0000000000010dc8 0 OBJECT LOCAL DEFAULT 18 __frame_dummy_init_array_entry
86-
52: 0000000000000858 0 NOTYPE LOCAL DEFAULT 17 $d
86+
52: 0000000000000860 0 NOTYPE LOCAL DEFAULT 17 $d
8787
53: 0000000000011030 0 NOTYPE LOCAL DEFAULT 24 $d
8888
54: 0000000000000000 0 FILE LOCAL DEFAULT ABS sync_write.c
8989
55: 0000000000000714 0 NOTYPE LOCAL DEFAULT 13 $x.0
9090
56: 0000000000011034 0 NOTYPE LOCAL DEFAULT 24 $d.1
9191
57: 000000000000002a 0 NOTYPE LOCAL DEFAULT 25 $d.2
92-
58: 00000000000008b8 0 NOTYPE LOCAL DEFAULT 17 $d.3
92+
58: 00000000000008c0 0 NOTYPE LOCAL DEFAULT 17 $d.3
9393
59: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
94-
60: 00000000000008e4 0 NOTYPE LOCAL DEFAULT 17 $d
95-
61: 00000000000008e4 0 OBJECT LOCAL DEFAULT 17 __FRAME_END__
94+
60: 00000000000008ec 0 NOTYPE LOCAL DEFAULT 17 $d
95+
61: 00000000000008ec 0 OBJECT LOCAL DEFAULT 17 __FRAME_END__
9696
62: 0000000000000000 0 FILE LOCAL DEFAULT ABS
9797
63: 0000000000010dd8 0 OBJECT LOCAL DEFAULT ABS _DYNAMIC
98-
64: 00000000000007f4 0 NOTYPE LOCAL DEFAULT 16 __GNU_EH_FRAME_HDR
98+
64: 00000000000007f8 0 NOTYPE LOCAL DEFAULT 16 __GNU_EH_FRAME_HDR
9999
65: 0000000000010fb8 0 OBJECT LOCAL DEFAULT ABS _GLOBAL_OFFSET_TABLE_
100100
66: 00000000000005a0 0 NOTYPE LOCAL DEFAULT 12 $x
101101
67: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34
@@ -107,19 +107,19 @@ Symbol table '.symtab' contains 92 entries:
107107
73: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 23 _edata
108108
74: 0000000000011038 4 OBJECT GLOBAL DEFAULT 24 z
109109
75: 0000000000011034 4 OBJECT GLOBAL DEFAULT 24 x
110-
76: 00000000000007dc 0 FUNC GLOBAL HIDDEN 14 _fini
110+
76: 00000000000007e0 0 FUNC GLOBAL HIDDEN 14 _fini
111111
77: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 __bss_end__
112112
78: 0000000000011020 0 NOTYPE GLOBAL DEFAULT 23 __data_start
113113
79: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
114114
80: 0000000000011028 0 OBJECT GLOBAL HIDDEN 23 __dso_handle
115115
81: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17
116-
82: 00000000000007f0 4 OBJECT GLOBAL DEFAULT 15 _IO_stdin_used
116+
82: 00000000000007f4 4 OBJECT GLOBAL DEFAULT 15 _IO_stdin_used
117117
83: 000000000001103c 4 OBJECT GLOBAL DEFAULT 24 secret
118118
84: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 _end
119119
85: 0000000000000600 52 FUNC GLOBAL DEFAULT 13 _start
120120
86: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 __end__
121121
87: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 24 __bss_start
122-
88: 0000000000000714 200 FUNC GLOBAL DEFAULT 13 main
122+
88: 0000000000000714 204 FUNC GLOBAL DEFAULT 13 main
123123
89: 0000000000011030 0 OBJECT GLOBAL HIDDEN 23 __TMC_END__
124124
90: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
125125
91: 0000000000000580 0 FUNC GLOBAL HIDDEN 11 _init

mill

+1-1
Original file line numberDiff line numberDiff line change
@@ -238,4 +238,4 @@ unset MILL_REPO_URL
238238

239239
# We don't quote MILL_FIRST_ARG on purpose, so we can expand the empty value without quotes
240240
# shellcheck disable=SC2086
241-
exec "${MILL}" $MILL_FIRST_ARG -D "mill.main.cli=${MILL_MAIN_CLI}" "$@"
241+
exec "${MILL}" $MILL_FIRST_ARG -D "mill.main.cli=${MILL_MAIN_CLI}" "$@"

0 commit comments

Comments
 (0)