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

check for load structure and included primops in rASL #121

Merged
merged 11 commits into from
Jan 21, 2025
Merged

Conversation

ailrst
Copy link

@ailrst ailrst commented Jan 9, 2025

This adds checks that

  1. Loads only appear in their own constant declarations
  2. We only emit intrinsics from a specific list

I expect I've missed some intrinsics that its possible to emit, I just included everything in coverage, cntlm + AtomicStart & AtomicEnd. I would be surprised if there aren't FP and vector intrinsics missing. E.g. the following all appear in mra but likely aren't all reachable in the lifter https://gist.github.com/ailrst/64ddbe6075f5c44a448626492f64a62c?

Some notes:

  • I put the check in dis_core, and pass the flag for whether to enable it by argument, this is possibly an uneccessarily messy change as it changes the signature of cpu and all the dis functions above dis_core, but it avoids another global flag. I did this partly because I was hoping to emit the trace only when the checks failed but I think I've misused the DisTrace (t, exc) exception. It at least captures all the possible entry-points to dis :)

  • Currently I just have a boolean flag to enable/disable all the checks, we could make this the list of checks to apply instead, but I'm not sure if we need that.

  • If there are other implicit guarantees on the rASL its worth adding checks including please let me know. Possibly the set of global identifiers?

@ncough
Copy link
Collaborator

ncough commented Jan 14, 2025

There are central lists for pure and impure primitive operations. It currently does not include the vector operations, but they should be added to the pure list.

@ncough
Copy link
Collaborator

ncough commented Jan 14, 2025

Great to see this! It would be nice to eventually also check the following, perhaps in later PRs:

  • Limit types to: bitvectors of constant width or booleans
  • Limit exprs to: Var, Field, Array, TApply, LitBits, LitInt, Slices
  • Limit statements to: VarDeclsNoInit, VarDecl, ConstDecl, TCall, Assign, Assert, Throw, If
  • Limit lexprs to: Var, Field, Array
  • Slices are always a single LoWd of constant values
  • If never has else if
  • Type arguments for calls are constant integers
  • No variable redeclaration

I'm sure there must be more than this, but can't immediately think of them. A more extreme validation may be to ensure the program type checks, but I am not sure if this is worthwhile.

@ncough
Copy link
Collaborator

ncough commented Jan 14, 2025

Not sure if this is the intention, but it would also be nice to run these between transforms for some sanity checks.

@ailrst
Copy link
Author

ailrst commented Jan 14, 2025

There are central lists for pure and impure primitive operations. It currently does not include the vector operations, but they should be added to the pure list.

I've added the extra bitvector, bool and vector functions to the pure list. I notice Elem.set and Elem.read are also emitted without the vectoriser enabled, so I'm wondering if they should be in either the pure or impure list in that case?

I also moved the prims check to after the vectoriser and removed the integer operations (e.g. mul_int in 0x0e011800 is emitted by dis_core) from the list on the assumption they were introduced by dis, if this is not the case I can add them back.

I agree it would be good to run the checks you list between passes.

@ailrst
Copy link
Author

ailrst commented Jan 15, 2025

I added the structural/syntactic checks so the remaining checks from the list you suggested are;

  • Limit types to: bitvectors of constant width or booleans
  • Type arguments for calls are constant integers
  • No variable redeclaration

type args will be easy but redeclaration and types will need to track context to check them so I'll leave them for another pr.

@ailrst ailrst marked this pull request as ready for review January 15, 2025 23:38
@ncough
Copy link
Collaborator

ncough commented Jan 17, 2025

I think we don't have to allow Expr_LitHex, but otherwise looks good to me.

@ncough ncough merged commit 7fe6e01 into partial_eval Jan 21, 2025
4 checks passed
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