Skip to content

Assume an x86_64 architecture for the machine model#1054

Merged
adpaco-aws merged 11 commits intomodel-checking:mainfrom
adpaco-aws:machine-model-audit
Apr 20, 2022
Merged

Assume an x86_64 architecture for the machine model#1054
adpaco-aws merged 11 commits intomodel-checking:mainfrom
adpaco-aws:machine-model-audit

Conversation

@adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Apr 15, 2022

Description of changes:

Checks that the target architecture is x86_84, prints a nice error otherwise. Also adds comments to the function building the machine model.

Should we add further requirements for the values coming from the session?

Resolved issues:

Resolves #64

Call-outs:

Testing:

  • How is this change tested? CI regression

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@adpaco-aws adpaco-aws requested a review from a team as a code owner April 15, 2022 14:48
tedinski
tedinski approved these changes Apr 15, 2022
View reviewed changes
@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Apr 15, 2022

Question: Do we want to also check here the values we get from the session? I am not sure if it's possible to get 32 as pointer_width for an x86_64 architecture, or in general a value we don't expect here (big endian, min. alignment > 1).

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Apr 19, 2022

I have used the commands here to obtain get the pointer_width values for all supported "x86_64-*" architectures:

x86_64-apple-darwin
  "target-pointer-width": "64",
x86_64-apple-ios
  "target-pointer-width": "64",
x86_64-apple-ios-macabi
  "target-pointer-width": "64",
x86_64-apple-tvos
  "target-pointer-width": "64",
x86_64-fortanix-unknown-sgx
  "target-pointer-width": "64",
x86_64-fuchsia
  "target-pointer-width": "64"
x86_64-linux-android
  "target-pointer-width": "64"
x86_64-pc-solaris
  "target-pointer-width": "64",
x86_64-pc-windows-gnu
  "target-pointer-width": "64",
x86_64-pc-windows-msvc
  "target-pointer-width": "64",
x86_64-sun-solaris
  "target-pointer-width": "64",
x86_64-unknown-dragonfly
  "target-pointer-width": "64"
x86_64-unknown-freebsd
  "target-pointer-width": "64"
x86_64-unknown-haiku
  "target-pointer-width": "64"
x86_64-unknown-hermit
  "target-pointer-width": "64",
x86_64-unknown-illumos
  "target-pointer-width": "64"
x86_64-unknown-l4re-uclibc
  "target-pointer-width": "64"
x86_64-unknown-linux-gnu
  "target-pointer-width": "64"
x86_64-unknown-linux-gnux32
  "target-pointer-width": "32"
x86_64-unknown-linux-musl
  "target-pointer-width": "64"
x86_64-unknown-netbsd
  "target-pointer-width": "64",
x86_64-unknown-none
  "target-pointer-width": "64"
x86_64-unknown-none-hermitkernel
  "target-pointer-width": "64"
x86_64-unknown-none-linuxkernel
  "target-pointer-width": "64"
x86_64-unknown-openbsd
  "target-pointer-width": "64"
x86_64-unknown-redox
  "target-pointer-width": "64"
x86_64-unknown-uefi
  "target-pointer-width": "64"
x86_64-uwp-windows-gnu
  "target-pointer-width": "64",
x86_64-uwp-windows-msvc
  "target-pointer-width": "64",
x86_64-wrs-vxworks
  "target-pointer-width": "64",

So there is at least one platform (x86_64-unknown-linux-gnux32) where the analysis would not be sound. Please note that custom targets can also be specified.

I have changed the original proposal so that the values we get from the session are checked against the ones we expect, in addition to these ones:

  • Add a new function check_target_arch_spec similar to check_options to specifically check target values that aren't really options.
  • Use /// for comment on machine_model_from_session
  • Add comments to point to relevant functions (from check_* to machine_model_* and vice versa).

I am requesting another review since the PR has changed substantially.

@adpaco-aws adpaco-aws requested review from celinval and tedinski April 19, 2022 16:40
@celinval
Copy link
Contributor

celinval commented Apr 19, 2022

I suggest that we restrict this to the following platforms:

  • x86_64-unknown-linux-gnu
  • x86_64-apple-darwin

A bunch of the platforms you listed are not even Tier 1 for the rustc compiler (https://doc.rust-lang.org/nightly/rustc/platform-support.html)

@tedinski
Copy link
Contributor

tedinski commented Apr 19, 2022

Yeah, FWIW, the Kani installer will only be working for those two platforms.

(Which reminds me, I should add an explicit check. Right now it's just fail to download a release bundle...)

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Apr 19, 2022

Agreed, updated the check to allow only these platforms.

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Apr 19, 2022

The regression for macOS fails because it does not detect x86_64-apple-darwin but x86_64-apple-macosx10.7.0. Not sure what to do now.

@tedinski
Copy link
Contributor

tedinski commented Apr 19, 2022

I'm adding the "nice" check to the installer in #1069

I think your original idea of asserting on "x86_64" and "64" on those original values is fine here.

@adpaco-aws
Copy link
Contributor Author

adpaco-aws commented Apr 20, 2022

I think your original idea of asserting on "x86_64" and "64" on those original values is fine here.

Thanks @tedinski , but I think we can keep this solution if we just check that session.target.llvm_target.starts_with("x86_64-apple-"). Please take a look.

celinval
celinval approved these changes Apr 20, 2022
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's definitely better than checking for just x86_64 and 64 bits. Too bad the MacOs had to be relaxed a bit. Thanks for doing this!

@adpaco-aws adpaco-aws merged commit 989604c into model-checking:main Apr 20, 2022
@adpaco-aws adpaco-aws mentioned this pull request Apr 26, 2022
Merged
4 tasks
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
@adpaco-aws @tedinski
Assume an x86_64 architecture for the machine model (model-checking#1054
3008076 
)

* Assume an x86_64 architecture for the machine model

* Add checks for arch spec/options

* Check platform instead of architecture

* Add debug statement

* print platform

* Use `starts_with` for apple platforms

* minor comment change

* Make code simpler
tedinski pushed a commit that referenced this pull request Apr 27, 2022
@adpaco-aws @tedinski
Assume an x86_64 architecture for the machine model (#1054)
fed674c 
* Assume an x86_64 architecture for the machine model

* Add checks for arch spec/options

* Check platform instead of architecture

* Add debug statement

* print platform

* Use `starts_with` for apple platforms

* minor comment change

* Make code simpler
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

2 more reviewers

@tedinski tedinski tedinski approved these changes

@celinval celinval celinval approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Ensure we are building the right machine model from a session

3 participants

@adpaco-aws @celinval @tedinski