Skip to content

Investigate why mir-linker test requires an unwind annotation #1978

Closed
#2301
Closed
Investigate why mir-linker test requires an unwind annotation#1978
#2301
Assignees
zhassan-aws
Labels
T-CBMCIssue related to an existing CBMC issueT-High PriorityTag issues that have high priority[C] InternalTracks some internal work. I.e.: Users should not be affected.
Milestone
Maintenance

Description

@zhassan-aws
zhassan-aws
opened on Dec 8, 2022

This is concerned with the mir-linker test (tests/cargo-kani/mir-linker/src/lib.rs).

Before CBMC 5.72.0, this test did not require an unwind annotation.

With CBMC 5.72.0, not specifying an unwind value causes it to unwind forever (see #1941).

Investigate why.

Activity

  1. zhassan-aws
    added
    [C] InternalTracks some internal work. I.e.: Users should not be affected.
    on Dec 8, 2022
  2. zhassan-aws
    assigned
    tautschnig
    on Dec 9, 2022

  3. tautschnig commented on Dec 9, 2022

    @tautschnig
    tautschnig
    on Dec 9, 2022
    Member

    It seems that we end up with a comparison to two constant-to-pointer type casts, where one of the constants (because of how we now do simplification) ends up have a different (but still perfectly correct) bitvector type. This fools a subsequent equality test. I'm trying to figure out how to make the equality test sufficiently smart.

  4. tautschnig
    added a commit that references this issue on Dec 12, 2022

    Simplify (T*)bitvector-constant to pointer-typed constant

    0ecf773

  5. tautschnig commented on Dec 12, 2022

    @tautschnig
    tautschnig
    on Dec 12, 2022
    Member

    Fixed in diffblue/cbmc#7427.

  6. tautschnig
    removed their assignment
    on Dec 14, 2022

  7. tautschnig commented on Dec 14, 2022

    @tautschnig
    tautschnig
    on Dec 14, 2022
    Member

    It seems that we end up with a comparison to two constant-to-pointer type casts, where one of the constants (because of how we now do simplification) ends up have a different (but still perfectly correct) bitvector type. This fools a subsequent equality test. I'm trying to figure out how to make the equality test sufficiently smart.

    On a second thought I have decided to discard the proposed change to CBMC. Instead, I started wondering where those pointer-typed constants with non-NULL value are coming from. It turns out Kani directly emitted that. From the symtab:

                  {
                "id": "struct",
                "sub": [
                  {
                    "id": "constant",
                    "namedSub": {
                      "value": {
                        "id": "FFFFFFFFFFFFFFFF"
                      },
                      "type": {
                        "id": "pointer",
                        "sub": [
                          {
                            "id": "unsignedbv",
                            "namedSub": {
                              "width": {
                                "id": "8"
                              }
                            }
                          }
                        ],
                        "namedSub": {
                          "width": {
                            "id": "64"
                          }
                        }
                      }
                    }
                  }
                ],
                "namedSub": {
                  "type": {
                    "id": "struct_tag",
                    "namedSub": {
                      "identifier": {
                        "id": "tag-_14121113017464461636"
                      }
                    }
                  }
                }
              }

    which in turn is the result of translating semver-1.0.14/src/identifier.rs around line 97. Does Rust have native pointer-typed numeric constants? In C, one would expect an integral value with a pointer type cast on top of it. Here, however, it seems that Kani generated a pointer with value 0xFFFFFFFFFFFFFFFF (and not a type cast of this integral constant to a pointer). It may still be necessary to do more work on the CBMC side, but I'd first ask that this use of pointer-typed constants be clarified.

  8. tedinski commented on Dec 14, 2022

    @tedinski
    tedinski
    on Dec 14, 2022
    Contributor

    Interesting. I expect the Rust compiler to try to maintain providence reasonably well, so I'm not (without digging in) where this is coming from. It could easily be mistranslation in Kani.

    I understand that in C you'd only ever get a pointer constant by writing an integer and casting it to a pointer type. Am I understanding you correctly that this is what you'd want for goto as well? If so, I think the validation should reject a raw pointer constant.

  9. tautschnig commented on Dec 14, 2022

    @tautschnig
    tautschnig
    on Dec 14, 2022
    Member

    I understand that in C you'd only ever get a pointer constant by writing an integer and casting it to a pointer type. Am I understanding you correctly that this is what you'd want for goto as well? If so, I think the validation should reject a raw pointer constant.

    We obviously lack a formalisation of GOTO programs at this point, but I'm not sure what semantics to attribute to a pointer-typed constant in the (not formalised) memory model of GOTO programs. The null-pointer constant we store as having a value of "NULL" (not zero!). The only other pointer-typed expression that I'd consider a legitimate constant is taking the address of an object.

  10. tedinski commented on Dec 21, 2022

    @tedinski
    tedinski
    on Dec 21, 2022
    Contributor

    Nominating this as high priority, since it might be a translation bug, and it should be simple to figure out (by asserting about types in the right constructor in our bindings)

  11. tedinski
    added
    T-High PriorityTag issues that have high priority
    on Dec 21, 2022

  12. zhassan-aws commented on Dec 22, 2022

    @zhassan-aws
    zhassan-aws
    on Dec 22, 2022
    ContributorAuthor

    Generating a pointer-typed numeric constant can be reproduced on this small program:

    #[cfg_attr(kani, kani::proof)]
fn main() {
    let _p = 0x0123456789ABCDEF as *const u8;
}

    Symbol table:

                                        {
                                        "id": "constant",
                                        "namedSub": {
                                            "value": {
                                                "id": "123456789ABCDEF"
                                            },
                                            "type": {
                                                "id": "pointer",
                                                "sub": [
                                                    {
                                                        "id": "unsignedbv",
                                                        "namedSub": {
                                                            "width": {
                                                                "id": "8"
                                                            }
                                                        }
                                                    }
                                                ],
                                                "namedSub": {
                                                    "width": {
                                                        "id": "64"
                                                    }
                                                }
                                            }
                                        }
                                    }

    The problem doesn't seem to be coming from MIR because the cast is explicit:
    The problem does seem to be coming from the MIR because it has a const literal of a pointer type:

    // Item: Fn(Instance { def: Item(WithOptConstParam { did: DefId(0:3 ~ pointer[3fe5]::main), const_param_did: None }), substs: [] })
// WARNING: This output format is intended for human consumers only
// and is subject to change without notice. Knock yourself out.
fn main() -> () {
    let mut _0: ();                      // return place in scope 0 at pointer.rs:2:11: 2:11
    let _1: *const u8;                   // in scope 0 at pointer.rs:3:9: 3:11
    scope 1 {
        debug _p => _1;                  // in scope 1 at pointer.rs:3:9: 3:11
    }

    bb0: {
        _1 = const {0x123456789abcdef as *const u8}; // scope 0 at pointer.rs:3:14: 3:45
                                         // mir::Constant
                                         // + span: pointer.rs:3:14: 3:45
                                         // + literal: Const { ty: *const u8, val: Value(Scalar(0x0123456789abcdef)) }
        return;                          // scope 0 at pointer.rs:4:2: 4:2
    }
}

    Specifically these lines in the comment:

                                             // mir::Constant
                                         // + span: pointer.rs:3:14: 3:45
                                         // + literal: Const { ty: *const u8, val: Value(Scalar(0x0123456789abcdef)) }

  13. zhassan-aws commented on Dec 22, 2022

    @zhassan-aws
    zhassan-aws
    on Dec 22, 2022
    ContributorAuthor

    This diff eliminates the pointer constant from the symbol table file generated by Kani:

    $ git diff
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 7756bc95229..0bc4a56fca9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -284,7 +284,8 @@ fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Ex
                 unreachable!("ZST is no longer represented as a scalar")
             }
             (Scalar::Int(_), ty::RawPtr(tm)) => {
-                Expr::pointer_constant(s.to_u64().unwrap(), self.codegen_ty(tm.ty).to_pointer())
+                Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64))
+                    .cast_to(self.codegen_ty(tm.ty).to_pointer())
             }

    The resulting symbol table for the mir-linker test becomes:

                                            "id": "typecast",
                                        "sub": [
                                            {
                                                "id": "constant",
                                                "namedSub": {
                                                    "value": {
                                                        "id": "FFFFFFFFFFFFFFFF"
                                                    },
                                                    "type": {
                                                        "id": "unsignedbv",
                                                        "namedSub": {
                                                            "width": {
                                                                "id": "64"
                                                            }
                                                        }
                                                    }
                                                }
                                            }
                                        ],
                                        "namedSub": {
                                            "type": {
                                                "id": "pointer",
                                                "sub": [
                                                    {
                                                        "id": "unsignedbv",
                                                        "namedSub": {
                                                            "width": {
                                                                "id": "8"
                                                            }
                                                        }
                                                    }
                                                ],
                                                "namedSub": {
                                                    "width": {
                                                        "id": "64"
                                                    }
                                                }
                                            }
                                        }

    The change passes regressions, but it does not eliminate the need to specify an unwind value. Not sure if I should create a PR for it. @tautschnig?

  14. tautschnig
    self-assigned this
    on Dec 22, 2022

  15. tautschnig commented on Dec 22, 2022

    @tautschnig
    tautschnig
    on Dec 22, 2022
    Member

    Adding this back onto my list. I'll try to see which additional changes might be necessary on the CBMC side.

  16. zhassan-aws commented on Dec 22, 2022

    @zhassan-aws
    zhassan-aws
    on Dec 22, 2022
    ContributorAuthor

    Thanks @tautschnig. And do you think it's still worthwhile to open a PR to switch to using a pointer cast for pointer constants?

  17. tautschnig
    added this to Kani 2023-01-23on Jan 3, 2023
  18. rahulku
    added this to the Maintenance milestone on Jan 5, 2023
  19. tautschnig
    added a commit that references this issue on Mar 1, 2023

    Byte-operator lowering: do not unconditionally insert bv cast

    a3f4730

  20. tautschnig commented on Mar 1, 2023

    @tautschnig
    tautschnig
    on Mar 1, 2023
    Member

    Thanks @tautschnig. And do you think it's still worthwhile to open a PR to switch to using a pointer cast for pointer constants?

    With apologies for taking this long to get back to this: yes, we do still want this fix to be merged. It might, however, be a good idea to combine it with a change to the test that drops the unwind annotation. That you can drop once diffblue/cbmc#7571 is merged into CBMC and the above fix to use pointer casts is applied.

  21. tautschnig
    added
    T-CBMCIssue related to an existing CBMC issue
    on Mar 1, 2023
  22. tautschnig
    assigned
    zhassan-aws
    and unassigned
    tautschnig
    on Mar 1, 2023
  23. tautschnig
    added 2 commits that reference this issue on Mar 2, 2023

    Byte-operator lowering: do not unconditionally insert bv cast

    b150633

    Byte-operator lowering: do not unconditionally insert bv cast

    f67691e
  24. tautschnig
    added a commit that references this issue on Mar 17, 2023

    Update CBMC version to 5.79.0

    07ba909
  25. tautschnig
    closed this as completedin #2301on Mar 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

T-CBMCIssue related to an existing CBMC issueT-High PriorityTag issues that have high priority[C] InternalTracks some internal work. I.e.: Users should not be affected.

Type

No type

Projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions