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

Added support for includes and functions in cat #736

Merged
merged 15 commits into from
Sep 16, 2024

Conversation

ThomasHaas
Copy link
Collaborator

@ThomasHaas ThomasHaas commented Sep 12, 2024

This PR is marked as DRAFT simply because there are currently no tests related this feature, and no existing .cat-files were updated. Otherwise, the PR is functional.

Added functionality:

  • include "filePath" now has semantics in .cat files.
  • Semantically, the included file (if it exists) is simply inlined into the including file (as if copy&pasted). If the file does not exist, we give a warning and treat it as NOOP.
  • The filePath is resolved relative to an optionally provided --cat.include=<includeDirectory> which defaults to DAT3M_HOME/cat.
  • Includes can be nested but there is no detection of recursive includes: those will likely cause recursion until out of memory.
  • Support for functions (see below)

If anyone (@hernan-poncedeleon ? :)) is interested in rewriting existing .cat files to make use of this feature, you are welcome to add to this PR. In particular, a simple basic.cat with definitions such as let poloc = po & loc would be nice to have so that we can remove a lot of hardcoded definitions from the Wmm class.

Possible other feature: I want to take a look into adding parametric definitions as in #733 to this PR but with a less invasive approach (i.e., purely implemented in the parser).

EDIT: I implemented functions/function calls in .cat. The support is very extensive:

  • Multiple parameter are allowed: let f(x, y) = x | y (though 0 parameters are currently unsupported)
  • Functions also work for unary sets:
let f(x, y) = x | y
let hb = f(com, po)
let M = f(R, W) 
  • Functions capture the context in which they were defined:
let z = oldDef
let f(x, y) = x | y | z // refers to the above defined z
let z = newDef
let a = f(b, c) // uses `oldDef` for z
  • Functions can be redefined just like relations
  • Functions can take complex arguments: let hb = f(po, f(co, f(rf, f(fr))))
  • Functions can call other functions: let g(x) = f(x, x). They cannot call themselves (recursion in functions is not allowed)

Commented out includes in LKMM because the included file contains unsupported features.
Commented out non-working include in aarch64.cat
@hernanponcedeleon
Copy link
Owner

If anyone (@hernan-poncedeleon ? :)) is interested in rewriting existing .cat files to make use of this feature, you are welcome to add to this PR. In particular, a simple basic.cat with definitions such as let poloc = po & loc would be nice to have so that we can remove a lot of hardcoded definitions from the Wmm class.

Do we want to keep treating ctrl, data, addr as "base" relations or should we define them as

let data = (idd^+) & (M * M)
let addr = (addrDirect | ((idd^+);addrDirect)) & (M * M)
let ctrl = ((idd^+);ctrlDirect) & (M * V)

Put it differently, do we want to get rid of all relations that make use of operators in Wmm.makePredefinedRelation()?

@ThomasHaas
Copy link
Collaborator Author

Possibly. The awkward part is that some of those base relations like idd are magical in that they argue about non-visible events. I'm not sure if we want to expose them.

@ThomasHaas ThomasHaas changed the title Added support for include statements in cat [DRAFT] Added support for includes and functions in cat [DRAFT] Sep 12, 2024
Fix cat grammar to make fencerel a valid function name
@ThomasHaas ThomasHaas changed the title Added support for includes and functions in cat [DRAFT] Added support for includes and functions in cat Sep 13, 2024
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
@hernanponcedeleon hernanponcedeleon merged commit 479e85e into development Sep 16, 2024
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the cat_parsing branch September 16, 2024 06:03
hernanponcedeleon pushed a commit that referenced this pull request Sep 16, 2024
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.

3 participants