sv-witnesses icon indicating copy to clipboard operation
sv-witnesses copied to clipboard

WIP: Proper handling of thread information in witness linter

Open SvenUmbricht opened this issue 2 years ago • 1 comments

Last year there were several threading-related issues with the linter which raised questions about the witness specification (cf. #30, #33, #36). This PR is to fix the handling of threading-related information in the linter.

SvenUmbricht avatar Oct 21 '21 09:10 SvenUmbricht

Even after the changes made in this PR check_function_stack still had some implicit assumptions about the witness that are not enforced by the specification and while trying to fix these I noticed some other issues / underspecifications that have to be resolved before this can be merged:

  • What if no thread id is specified on a given edge? A previous version of the specification stated

    If no threadId is given, any thread can be active

    but this line has been removed in 232349268b63886b8955a66e96b143127c8554b4. The current state of this PR is to treat edges without a thread id as if the id of the main thread was specified.

  • How to interpret edges having data elements with both enterFunction and returnFromFunction keys? When checking callstack validity the linter assumes function returns to happen first, because otherwise a transition with different values for enterFunction and returnFromFunction would always be invalid.

SvenUmbricht avatar Oct 29 '21 11:10 SvenUmbricht