Skip to content
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

feat(handle_t): redef handle_t as pointer #16

Merged
merged 2 commits into from
Aug 24, 2022

Conversation

priyasiddharth
Copy link
Collaborator

  • Add a "HANDLE_TYPE_IS_PTR" compile flag that
    redefines handle_t as ptr (instead of int32).

  • Create a local copy of storage/ipc.c in trusty_mod directory to allow handle_t to be treated as an opaque object.

  • Create a local include dir with trusty_ipc.h for the actual handle_t is ptr redef.

  • Run port_create_destroy_harness and msg_buffer_harness with redefined handle_t on
    local ipc.c

  • Add handle is ptr jobs to CI

Known issues/Needs investigation:

The following issues need to be fixed but not blocking the PR since the infrastructure changes are quite big itself.

  • msg_buffer_harness.c fails in vac mode with handle_t as ptr. It seems to be failing at head (added to CI blacklist) so this PR doesn't make the situation worse.
  • wait_any gets a valid handle from sea_handle_table.c. We store valid handles in an array. This needs to be likely unrolled.

@@ -63,7 +70,11 @@ include_directories(${TRUSTY_ROOT}/trusty/user/base/interface/keymaster/include)
include_directories(${TRUSTY_ROOT}/trusty/user/base/interface/hwkey/include)
include_directories(${TRUSTY_ROOT}/trusty/user/base/include/uapi)
include_directories(${TRUSTY_ROOT}/trusty/user/base/include/shared)
include_directories(${TRUSTY_ROOT}/trusty/user/base/include/user)
if (HANDLE_TYPE_IS_PTR)
Copy link
Collaborator

Choose a reason for hiding this comment

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

@priyasiddharth you can also add HANDLE_TYPE_IS_PTR to definitions using CMake add_definitions command and then use it as #ifdef inside header files. This might be simpler than changing include directories with cmake.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

A simple solution would delegate the decision to each include point and would duplicate the conditional for evey use. A more complex solution would be to have a wrapper header which makes the decision internally. It's not clear why that's needed for now.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I was suggesting a wrapper header, simply because this is the typical way to address this problem. This guarantees less unexpected issues later on.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We discussed this in https://seahornteam.slack.com/archives/DPND2KEJU/p1659124357825129.

conclusion: to use wrap header file you would need to merge common files rather than have two completely different source trees

This requires adding more moving pieces to the build and IMO is overkill for now. My vote is to submit this PR and revisit this if it needs more engineering to make it robust -- once it moves beyond being a proof of concept.

@priyasiddharth
Copy link
Collaborator Author

Fixed. PTAL @agurfinkel

seahorn/sea_base.yaml Outdated Show resolved Hide resolved
seahorn/sea.yaml Outdated Show resolved Hide resolved
else ()
add_subdirectory(libc-trusty)
endif ()
add_compile_definitions(CAN_RETURN_INVALID_IPC_HANDLE=0)
Copy link
Collaborator

Choose a reason for hiding this comment

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

are there multiple conflicting compiler definitions? Are you assuming they are resolved somehow by CMake or by the compiler?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

In the original spec (impl), some jobs are written assuming a valid handle_t is always returned by the environment. Other jobs account for failure. I have added this compile_definition to control what the environment will return per job.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I noticed that this definition is added multiple times in different CMakeLists.txt files. I am asking how the exclusivity of which definition is active is maintained.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The short answer is that exclusivity is maintained by user discipline. Each directory of jobs is independent of other jobs hence there should not be a conflict.

--
The problem is that this can cause silent unexpected behaviour if user breaks discipline or jobs are rearchitected to be dependent on each other. One solution is to move to the target based compilation model instead of the directory one used now. In doing so we can ensure that dependencies are explicit and there are known (few) points where a token can redefined. Right now, each directory can redefine a token which can become hard to reason about.

Changing the compilation model seems out of scope in this PR.

* Add a "HANDLE_TYPE_IS_PTR" compile flag that
redefines handle_t as ptr (instead of int32).

* Create a local copy of storage/ipc.c in trusty_mod directory to allow handle_t to be treated as an opaque object.

* Create a local include dir with trusty_ipc.h for the actual handle_t is ptr redef.

* Run port_create_destroy_harness and msg_buffer_harness with redefined handle_t on
local ipc.c

* Add handle is ptr jobs to CI

Known issues/Needs investigation:

The following issues need to be fixed but not blocking the PR since the infrastructure changes are quite big itself.

* msg_buffer_harness.c fails in vac mode with handle_t as ptr. It seems to be failing at head (added to CI blacklist) so this PR doesn't make the situation worse.
@priyasiddharth
Copy link
Collaborator Author

PTAL.

cex mode hangs for two jobs:

  1. port_send_msg verification hangs in cex mode with handle_type_is_ptr=on #19
  2. port_create_destroy verification hangs in handle_type_is_ptr _ cex mode  #18

Given the number of moving pieces in the PR and that it suffices a robust proof of concept, my preference is to submit this PR and resolve the remaining issues separately.

@priyasiddharth
Copy link
Collaborator Author

ping...

Is this blocked on something from me?

@agurfinkel
Copy link
Collaborator

no. please merge

@priyasiddharth priyasiddharth merged commit bd84d22 into seahorn:master Aug 24, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants