2021 week 34: rebase off upstream #437

adpaco-aws · 2021-08-18T10:54:42Z

No description provided.

celinval · 2021-08-31T22:59:53Z

Trying out merge instead of rebase. The merge itself was clean. There were a few API changes that required adjustments to RMC code. Now I am trying to get the regression working. It looks like there is some issue identifying the line where an assert is. I'm trying to fix that before submitting the merge.

> ./scripts/rmc-regression.sh
Updating only changed submodules
Submodules updated in 0.01 seconds
    Finished dev [unoptimized + debuginfo] target(s) in 0.11s
skip untracked path src/test/cargo-rmc/simple-extern/target/ during rustfmt invocations
skip untracked path src/test/cargo-rmc/simple-lib/target/ during rustfmt invocations
skip untracked path src/test/expected/enum/main.goto during rustfmt invocations
skip untracked path src/test/expected/enum/main.json during rustfmt invocations
Build completed successfully in 0:00:02
Updating only changed submodules
Submodules updated in 0.01 seconds
    Finished dev [unoptimized + debuginfo] target(s) in 0.10s
Building stage0 std artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
    Finished release [optimized + debuginfo] target(s) in 0.10s
Copying stage0 std from stage0 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Building stage0 compiler artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
warning: unused import: `CodegenResults`
 --> compiler/rustc_codegen_ssa/src/traits/backend.rs:4:13
  |
4 | use crate::{CodegenResults, ModuleCodegen};
  |             ^^^^^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

warning: `rustc_codegen_ssa` (lib) generated 1 warning
warning: function is never used: `time_trace_profiler_finish`
   --> compiler/rustc_codegen_llvm/src/llvm_util.rs:152:8
    |
152 | pub fn time_trace_profiler_finish(file_name: &str) {
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: `#[warn(dead_code)]` on by default

warning: `rustc_codegen_llvm` (lib) generated 1 warning
warning: associated function is never used: `process_rlink`
   --> compiler/rustc_driver/src/lib.rs:596:8
    |
596 |     fn process_rlink(sess: &Session, compiler: &interface::Compiler) -> Result<(), ErrorReported> {
    |        ^^^^^^^^^^^^^
    |
    = note: `#[warn(dead_code)]` on by default

warning: `rustc_driver` (lib) generated 1 warning
    Finished release [optimized + debuginfo] target(s) in 0.15s
Copying stage0 rustc from stage0 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Assembling stage1 compiler (x86_64-unknown-linux-gnu)
Building stage1 std artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
    Finished release [optimized + debuginfo] target(s) in 0.12s
Copying stage1 std from stage1 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Build completed successfully in 0:00:01
Updating only changed submodules
Submodules updated in 0.01 seconds
    Finished dev [unoptimized + debuginfo] target(s) in 0.11s
Building stage0 std artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
    Finished release [optimized + debuginfo] target(s) in 0.11s
Copying stage0 std from stage0 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Building stage0 compiler artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
warning: unused import: `CodegenResults`
 --> compiler/rustc_codegen_ssa/src/traits/backend.rs:4:13
  |
4 | use crate::{CodegenResults, ModuleCodegen};
  |             ^^^^^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

warning: `rustc_codegen_ssa` (lib) generated 1 warning
warning: function is never used: `time_trace_profiler_finish`
   --> compiler/rustc_codegen_llvm/src/llvm_util.rs:152:8
    |
152 | pub fn time_trace_profiler_finish(file_name: &str) {
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: `#[warn(dead_code)]` on by default

warning: `rustc_codegen_llvm` (lib) generated 1 warning
warning: associated function is never used: `process_rlink`
   --> compiler/rustc_driver/src/lib.rs:596:8
    |
596 |     fn process_rlink(sess: &Session, compiler: &interface::Compiler) -> Result<(), ErrorReported> {
    |        ^^^^^^^^^^^^^
    |
    = note: `#[warn(dead_code)]` on by default

warning: `rustc_driver` (lib) generated 1 warning
    Finished release [optimized + debuginfo] target(s) in 0.16s
Copying stage0 rustc from stage0 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Assembling stage1 compiler (x86_64-unknown-linux-gnu)
Building stage1 std artifacts (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)
    Finished release [optimized + debuginfo] target(s) in 0.10s
Copying stage1 std from stage1 (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu / x86_64-unknown-linux-gnu)
Building stage0 tool compiletest (x86_64-unknown-linux-gnu)
    Finished release [optimized + debuginfo] target(s) in 0.11s
Check compiletest suite=cbmc mode=rmc (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)

running 209 tests
iiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiii 100/209
iiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiii 200/209
iiiiiiiii
test result: ok. 0 passed; 0 failed; 209 ignored; 0 measured; 0 filtered out; finished in 0.00s

	finished in 0.182 seconds
Check compiletest suite=firecracker mode=rmc (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)

running 3 tests
iii
test result: ok. 0 passed; 0 failed; 3 ignored; 0 measured; 0 filtered out; finished in 0.00s

	finished in 0.047 seconds
Check compiletest suite=prusti mode=rmc (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)

running 8 tests
iiiiiiii
test result: ok. 0 passed; 0 failed; 8 ignored; 0 measured; 0 filtered out; finished in 0.00s

	finished in 0.047 seconds
Check compiletest suite=smack mode=rmc (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)

running 40 tests
iiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiii
test result: ok. 0 passed; 0 failed; 40 ignored; 0 measured; 0 filtered out; finished in 0.00s

	finished in 0.048 seconds
Check compiletest suite=expected mode=expected (x86_64-unknown-linux-gnu -> x86_64-unknown-linux-gnu)

running 37 tests
iiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiFFF
failures:

---- [expected] expected/niche/main.rs stdout ----

error: test failed: expected output to contain the line: line 21 assertion failed: false: SUCCESS
status: exit status: 0
command: "rmc" "--input" "/tmp/rmc/src/test/expected/niche/main.rs" "--cbmc-args"
stdout:
------------------------------------------
CBMC version 5.30.1 (cbmc-5.30.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /tmp/rmc/src/test/expected/niche/main.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1  thread 0
Runtime Symex: 0.0034986s
size of program expression: 157 steps
simple slicing removed 21 assignments
Generated 26 VCC(s), 9 remaining after simplification
Runtime Postprocess Equation: 1.0699e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00051053s
Running propositional reduction
Post-processing
Runtime Post-process: 1.1648e-05s
Solving with MiniSAT 2.2.1 with simplifier
1295 variables, 71 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 2.1194e-05s
Runtime decision procedure: 0.00056827s

** Results:
/tmp/rmc/src/test/expected/niche/main.rs function get_opt
[get_opt.pointer_arithmetic.1] line 11 pointer arithmetic: dead object in (unsigned char *)&var_0 + 8: SUCCESS
[get_opt.pointer_dereference.1] line 11 dereference failure: dead object in *((unsigned char **)((unsigned char *)&var_0 + 8)): SUCCESS

/tmp/rmc/src/test/expected/niche/main.rs function get_some
[get_some.pointer_dereference.1] line 15 dereference failure: pointer NULL in *a: SUCCESS
[get_some.pointer_dereference.2] line 15 dereference failure: pointer invalid in *a: SUCCESS
[get_some.pointer_dereference.3] line 15 dereference failure: deallocated dynamic object in *a: SUCCESS
[get_some.pointer_dereference.4] line 15 dereference failure: dead object in *a: SUCCESS
[get_some.pointer_dereference.5] line 15 dereference failure: pointer outside object bounds in *a: SUCCESS
[get_some.pointer_dereference.6] line 15 dereference failure: invalid integer address in *a: SUCCESS

/tmp/rmc/src/test/expected/niche/main.rs function main
[main.assertion.1] line 20 assertion failed: false: SUCCESS
[main.assertion.2] line 20 unreachable code: SUCCESS
[main.pointer_arithmetic.1] line 20 pointer arithmetic: dead object in (unsigned char *)&x + 8: SUCCESS
[main.pointer_dereference.1] line 20 dereference failure: dead object in *((unsigned char **)((unsigned char *)&x + 8)): SUCCESS
[main.assertion.3] line 25 unreachable code: SUCCESS
[main.assertion.4] line 25 assertion failed: false: SUCCESS
[main.pointer_arithmetic.2] line 25 pointer arithmetic: dead object in (unsigned char *)&var_4 + 8: SUCCESS
[main.pointer_dereference.2] line 25 dereference failure: dead object in *((unsigned char **)((unsigned char *)&var_4 + 8)): SUCCESS
[main.assertion.5] line 27 assertion failed: a == *b: SUCCESS
[main.pointer_dereference.3] line 27 dereference failure: pointer NULL in *b: SUCCESS
[main.pointer_dereference.4] line 27 dereference failure: pointer invalid in *b: SUCCESS
[main.pointer_dereference.5] line 27 dereference failure: deallocated dynamic object in *b: SUCCESS
[main.pointer_dereference.6] line 27 dereference failure: dead object in *b: SUCCESS
[main.pointer_dereference.7] line 27 dereference failure: pointer outside object bounds in *b: SUCCESS
[main.pointer_dereference.8] line 27 dereference failure: invalid integer address in *b: SUCCESS

** 0 of 23 failed (1 iterations)
VERIFICATION SUCCESSFUL


------------------------------------------
stderr:
------------------------------------------

------------------------------------------


---- [expected] expected/enum/main.rs stdout ----

error: test failed: expected output to contain the line: line 19 assertion failed: false: SUCCESS
status: exit status: 10
command: "rmc" "--input" "/tmp/rmc/src/test/expected/enum/main.rs" "--cbmc-args"
stdout:
------------------------------------------
CBMC version 5.30.1 (cbmc-5.30.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /tmp/rmc/src/test/expected/enum/main.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00247615s
size of program expression: 128 steps
simple slicing removed 4 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 1.1601e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000538399s
Running propositional reduction
Post-processing
Runtime Post-process: 1.7364e-05s
Solving with MiniSAT 2.2.1 with simplifier
1281 variables, 35 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000136132s
Runtime decision procedure: 0.000706007s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
1281 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 3.312e-06s
Runtime decision procedure: 8.999e-06s

** Results:
/tmp/rmc/src/test/expected/enum/main.rs function main
[main.assertion.1] line 18 assertion failed: false: SUCCESS
[main.assertion.2] line 18 unreachable code: SUCCESS
[main.assertion.3] line 19 assertion failed: x == 10: SUCCESS
[main.assertion.4] line 22 unreachable code: SUCCESS
[main.assertion.5] line 22 assertion failed: false: SUCCESS
[main.assertion.6] line 25 assertion failed: x == 30 && y == 60.0: SUCCESS
[main.assertion.7] line 26 assertion failed: x == 31: FAILURE

** 1 of 7 failed (2 iterations)
VERIFICATION FAILED


------------------------------------------
stderr:
------------------------------------------

------------------------------------------


---- [expected] expected/niche2/main.rs stdout ----

error: test failed: expected output to contain the line: line 22 assertion failed: false: SUCCESS
status: exit status: 10
command: "rmc" "--input" "/tmp/rmc/src/test/expected/niche2/main.rs" "--cbmc-args"
stdout:
------------------------------------------
CBMC version 5.30.1 (cbmc-5.30.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /tmp/rmc/src/test/expected/niche2/main.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00315528s
size of program expression: 143 steps
simple slicing removed 17 assignments
Generated 12 VCC(s), 9 remaining after simplification
Runtime Postprocess Equation: 9.389e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000439357s
Running propositional reduction
Post-processing
Runtime Post-process: 1.916e-05s
Solving with MiniSAT 2.2.1 with simplifier
1004 variables, 33 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000128217s
Runtime decision procedure: 0.00060695s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
1004 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 4.641e-06s
Runtime decision procedure: 1.3452e-05s

** Results:
/tmp/rmc/src/test/expected/niche2/main.rs function get_none
[get_none.pointer_arithmetic.1] line 9 pointer arithmetic: dead object in (unsigned char *)&var_0 + 0: SUCCESS
[get_none.pointer_dereference.1] line 9 dereference failure: dead object in *((unsigned int *)((unsigned char *)&var_0 + 0)): SUCCESS

/tmp/rmc/src/test/expected/niche2/main.rs function main
[main.assertion.1] line 21 assertion failed: false: SUCCESS
[main.assertion.2] line 21 unreachable code: SUCCESS
[main.overflow.1] line 21 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_1 + 0)) - 2: SUCCESS
[main.pointer_arithmetic.1] line 21 pointer arithmetic: dead object in (unsigned char *)&var_1 + 0: SUCCESS
[main.pointer_dereference.1] line 21 dereference failure: dead object in *((unsigned int *)((unsigned char *)&var_1 + 0)): SUCCESS
[main.overflow.2] line 26 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_3 + 0)) - 2: FAILURE
[main.pointer_arithmetic.2] line 26 pointer arithmetic: dead object in (unsigned char *)&var_3 + 0: SUCCESS
[main.pointer_dereference.2] line 26 dereference failure: dead object in *((unsigned int *)((unsigned char *)&var_3 + 0)): SUCCESS
[main.assertion.4] line 27 assertion failed: x == 10: SUCCESS
[main.assertion.3] line 28 assertion failed: false: SUCCESS
[main.overflow.3] line 31 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_10 + 0)) - 2: FAILURE
[main.pointer_arithmetic.3] line 31 pointer arithmetic: dead object in (unsigned char *)&var_10 + 0: SUCCESS
[main.pointer_dereference.3] line 31 dereference failure: dead object in *((unsigned int *)((unsigned char *)&var_10 + 0)): SUCCESS
[main.assertion.5] line 33 assertion failed: false: SUCCESS

** 2 of 16 failed (2 iterations)
VERIFICATION FAILED


------------------------------------------
stderr:
------------------------------------------

------------------------------------------



failures:
    [expected] expected/enum/main.rs
    [expected] expected/niche/main.rs
    [expected] expected/niche2/main.rs

test result: FAILED. 0 passed; 3 failed; 34 ignored; 0 measured; 0 filtered out; finished in 0.15s

Some tests failed in compiletest suite=expected mode=expected host=x86_64-unknown-linux-gnu target=x86_64-unknown-linux-gnu

expected success, got: exit status: 1


Build completed unsuccessfully in 0:00:01

Required manual fix due to API changes: - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/monomorphize/collector.rs Updated test expectations due to issue model-checking#466: - src/test/expected/enum/expected - src/test/expected/niche/expected - src/test/expected/niche2/expected

Required manual fix due to API changes: - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/monomorphize/collector.rs Updated test expectations due to issue #466: - src/test/expected/enum/expected - src/test/expected/niche/expected - src/test/expected/niche2/expected

Required manual fix due to API changes: - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/monomorphize/collector.rs Updated test expectations due to issue model-checking#466: - src/test/expected/enum/expected - src/test/expected/niche/expected - src/test/expected/niche2/expected

Required manual fix due to API changes: - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/goto_ctx.rs - compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/monomorphize/collector.rs Updated test expectations due to issue #466: - src/test/expected/enum/expected - src/test/expected/niche/expected - src/test/expected/niche2/expected

adpaco-aws added Area: build Z-Sync Upstream Fetch changes from rustc repository. Old Rebase labels Aug 18, 2021

adpaco-aws self-assigned this Aug 18, 2021

adpaco-aws assigned celinval Aug 31, 2021

celinval closed this as completed Sep 7, 2021

github-actions bot mentioned this issue Feb 11, 2025

Toolchain upgrade to nightly-2025-02-11 failed #3884

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

2021 week 34: rebase off upstream #437

2021 week 34: rebase off upstream #437

adpaco-aws commented Aug 18, 2021

celinval commented Aug 31, 2021

2021 week 34: rebase off upstream #437

2021 week 34: rebase off upstream #437

Comments

adpaco-aws commented Aug 18, 2021

celinval commented Aug 31, 2021