-
Notifications
You must be signed in to change notification settings - Fork 3
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
411 simple integration test using old simple rust programs #413
Merged
Merged
Changes from all commits
Commits
Show all changes
32 commits
Select commit
Hold shift + click to select a range
5de3075
Add Rust test programs from prior repo to test data
jberthold 97a6bac
make all programs compile and run without errors/warnings/output
jberthold c39bf1f
Fix two typos in symbol names
jberthold 33a7193
Add error messages to some assertions in the parser
jberthold 02ec008
submodule setup for smir_pretty, simple make target for parse tests
jberthold 6bdd7ea
Add CI job to test integration with smir_pretty
jberthold 0356f7d
Merge remote-tracking branch 'origin/master' into 411-salvage-old-rus…
jberthold 342af6b
Set Version: 0.3.41
ad9bb8d
rename container for smir integration test
jberthold c121268
tweak dependency on rust compiler source
jberthold c1820a5
tweak dependency on rust compiler source again, use github-native rust
jberthold 2ec3f6e
use 3rd-party rustc setup action (want nightly)
jberthold 1a46f69
attempt to work around CI-build logic in rustc bootstrap
jberthold a6b90ee
Set Version: 0.3.42
243e2ae
attempt to work around CI-build logic in rustc bootstrap - stage 2
jberthold 94b6ad9
Merge remote-tracking branch 'origin/master' into 411-salvage-old-rus…
jberthold 14e32dd
Set Version: 0.3.42
2683c37
remove config.toml experiment
jberthold 498d006
lie to rustc bootstrap that we are not in CI (modify GITHUB_ACTIONS v…
jberthold aaeda05
another way to modify GITHUB_ACTIONS
jberthold b79f1db
tests not test
jberthold 8a3196c
rearrange steps to run the tests within docker (with K available)
jberthold 770646f
pin nightly rustc to today's date
jberthold 7a1c632
add caching for rust artefacts
jberthold 0d35a8e
Formatting of all steps
jberthold 116585e
use yesterday's date, as I am ahead of the world
jberthold 529be01
different syntax for pinned nightly toolchain
jberthold 731bdcc
add build dir to rust cache
jberthold 125cb5e
actually fail on smir errors or parse errors
jberthold 3a1ddb3
HACK: patch rustc_arch.sh script in docker so we can run smir_pretty
jberthold ebac227
patching the patch
jberthold bee05d5
correct symbols for MonoItems (kast requires use of append/empty)
jberthold File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
[submodule "deps/smir_pretty"] | ||
path = deps/smir_pretty | ||
url = https://github.com/runtimeverification/smir_pretty |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Submodule smir_pretty
added at
dcc656
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,3 @@ | ||
from typing import Final | ||
|
||
VERSION: Final = '0.3.41' | ||
VERSION: Final = '0.3.42' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn main() { | ||
let a = [1, 2, 3, 4]; | ||
|
||
assert!(a == [1, 2, 3, 4]); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
fn main() { | ||
let a = 42; | ||
let b = 3 + 39; | ||
|
||
assert_eq!(b, a); | ||
} |
5 changes: 5 additions & 0 deletions
5
kmir/src/tests/integration/data/run-rs/closures/closure-args.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn main() { | ||
let sum = |x, y| -> i32 { x + y }; | ||
|
||
assert!(sum(20, 22) == 42); | ||
} |
5 changes: 5 additions & 0 deletions
5
kmir/src/tests/integration/data/run-rs/closures/closure-no-args.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn main() { | ||
let sum = || -> u32 { 42 }; | ||
|
||
assert!(sum() == 42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
#![allow(unused)] | ||
#![allow(dead_code)] | ||
enum Letter { | ||
A, | ||
B, | ||
} | ||
|
||
fn main() { | ||
let a = Letter::A; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
fn main() { | ||
let a:f32 = 3.5; | ||
let b:f32 = 1.2; | ||
|
||
assert!(a + b == 4.7); | ||
|
||
let c:f64 = 3.5; | ||
let d:f64 = 1.2; | ||
|
||
assert!(c + d == 4.7); | ||
} |
23 changes: 23 additions & 0 deletions
23
kmir/src/tests/integration/data/run-rs/functions/sum-to-n.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
fn sum_to_n(n:usize) -> usize { | ||
let mut sum = 0; | ||
let mut counter = n; | ||
|
||
while counter > 0 { | ||
sum += counter; | ||
counter = counter - 1; | ||
} | ||
return sum; | ||
} | ||
|
||
fn test_sum_to_n() -> () { | ||
let n = 10; | ||
let golden = 55; | ||
let sucess = sum_to_n(n) == golden; | ||
assert!(sucess); | ||
} | ||
|
||
|
||
fn main() { | ||
test_sum_to_n(); | ||
return (); | ||
} |
14 changes: 14 additions & 0 deletions
14
kmir/src/tests/integration/data/run-rs/generics/generic.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
fn index_slice<T>(slice:&[T], index: usize) -> &T { | ||
&(slice[index]) | ||
} | ||
|
||
fn main() { | ||
let numbers = [1, 2, 3, 4, 5]; | ||
let letters = ['a', 'b', 'c', 'd', 'e']; | ||
|
||
let middle_number:&i32 = index_slice(&numbers[..], 2); | ||
let middle_letter:&char = index_slice(&letters[..], 2); | ||
|
||
assert!(*middle_number == 3); | ||
assert!(*middle_letter == 'c'); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,74 @@ | ||
fn test_binop(x:i32, y:i32) -> () { | ||
// Arithmetic | ||
// Addition | ||
assert!(x + y == 52); | ||
assert!(52 == x + y); | ||
assert!(x + y == y + x); | ||
|
||
// Subtraction | ||
assert!(x - y == 32); | ||
assert!(y - x == -32); | ||
assert!(y - x != x - y); | ||
|
||
// Multiplication | ||
assert!(x * y == 420); | ||
assert!(x * -y == -420); | ||
assert!(-x * y == -420); | ||
assert!(-x * -y == 420); | ||
|
||
// Division | ||
// assert!(420 / 10 == 42); // FAILING SEE div.rs and div.mir | ||
|
||
// Modulo | ||
// assert!(x % 10 == 2); // FAILING SEE modulo.rs and modulo.mir | ||
|
||
// Bitwise | ||
// Xor | ||
assert!(1 ^ 2 == 3); | ||
assert!(1 ^ 3 == 2); | ||
|
||
// Or | ||
assert!(1 | 2 == 3); | ||
assert!(1 | 3 == 3); | ||
|
||
// And | ||
assert!(1 & 2 == 0); | ||
assert!(1 & 3 == 1); | ||
|
||
// // Shl | ||
assert!(2 << 1 == 4); | ||
// assert!(-128_i8 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir | ||
// assert!(-32768_i16 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir | ||
// assert!(-2147483648_i32 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir | ||
// assert!(-9223372036854775808_i64 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir | ||
// assert!(-17014118346046923173168730371588410572_i128 << 1 == 0); FAILS SEE shl_min.rs and shl_min.mir | ||
|
||
|
||
// // Shr | ||
assert!(2 >> 1 == 1); | ||
assert!(3 >> 1 == 1); | ||
assert!(1 >> 1 == 0); | ||
|
||
// Comparisions | ||
// Less Then | ||
assert!(x < x + y); | ||
|
||
// Less Then or Equal | ||
assert!(x <= x + y); | ||
assert!(x <= x + y - y); | ||
|
||
// Greater Then | ||
assert!(x + y > x); | ||
|
||
// Greater Then or Equal | ||
assert!(x + y >= x); | ||
assert!(x + y - y >= x); | ||
} | ||
|
||
|
||
fn main() { | ||
let x = 42; | ||
let y = 10; | ||
test_binop(x, y); | ||
return (); | ||
} |
12 changes: 12 additions & 0 deletions
12
kmir/src/tests/integration/data/run-rs/integers/const-arithm-simple.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
fn test(x: usize, y:usize) -> bool { | ||
return x > y; | ||
} | ||
|
||
|
||
fn main() { | ||
let x:usize = 42; | ||
let y:usize = 0; | ||
let z:bool = test(x, y); | ||
assert!(z); | ||
return (); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
fn main() { | ||
assert!(420 / 10 ==42); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
fn main() { | ||
assert!(42 % 10 == 2); | ||
} |
5 changes: 5 additions & 0 deletions
5
kmir/src/tests/integration/data/run-rs/integers/primitive-type-bounds.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn main () { | ||
let a:u32 = 4294967295; | ||
let b:u32 = 4294967294 + 1; | ||
assert!(a == b) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
fn main() { | ||
assert!(-128_i8 << 1 == 0); | ||
assert!(-32768_i16 << 1 == 0); | ||
assert!(-2147483648_i32 << 1 == 0); | ||
assert!(-9223372036854775808_i64 << 1 == 0); | ||
assert!(-170141183460469231731687303715884105728_i128 << 1 == 0); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
fn main() { | ||
let a = Box::new(5); | ||
let b = Box::new(5); | ||
|
||
assert!(a == b); | ||
assert!(*a == *b); | ||
assert!(*a == 5); | ||
// assert!(a == 5); // Not possible to equate Box::(Type) with Type | ||
} |
6 changes: 6 additions & 0 deletions
6
kmir/src/tests/integration/data/run-rs/option/option-construction.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
#![allow(unused)] | ||
fn main() { | ||
let a:Option<u32> = Some(42); | ||
let b:Option<u32> = None; | ||
let c:u32 = a.unwrap(); | ||
} |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@jberthold This is the hack to get our version of rustc running for smir pretty on CI?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes. The problem is that we need to run inside the docker image (to have
kompile
) but there is norustup
in the image. That script usesrustup
to findrustc
, then callsrustc
just to find out the target architecture string (which is part of the path to the libraries to link to). ➰ ➿The hack is to find that architecture string outside the docker image and then patch the script inside the docker image's file system (which is not shared with the host for some other reason... 🤷 ) to print that string
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay my understanding is that this will not need to rebuild the stage 2 compiler from our semantics from consecutive runs of the tests, and even if the K source is changed as the semantics will kompile but the stage 2 compiler is already built.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I even think the entire set of compiler artefacts could be cached, and tried to set up a cache for it, but the compiler build setup is multi-stage and therefore more complex to avoid rebuilds. For now this was just supposed to be the first step - our setup with the compiler dependency is definitely "suboptimal" anyway (and should/will change soon).