-
Notifications
You must be signed in to change notification settings - Fork 3
Initialise a call config in python (with symbolic arguments) #584
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
Conversation
Previous constructor becomes a utility `from_file`
…REAKS TESTS" This reverts commit 9e44a4c. Left the `run_call` function in place as it may be useful at some point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks really good to me overall! Some things it makes me think about:
- Probably
parser
submodule should be directly importing and using theSMIRInfo
class, rather than us passing in the JSON directly to it. The parser can then use the extracting helpers to get the info it needs for parsing. - I'm not super happy with how stateful
ArgGenerator
is, but it seems like it's totally encapsulated bysymbolic_locals
as a function, so it should be OK as long as we don't start passing aroundArgGenerator
s as arguments to things.
Realized we missed something and didn't have tests catching it.
@jberthold can you add tests of the new functionality? Specifically, of calling a function with arguments? You can add it to the |
if not sym in fun_syms: | ||
continue |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this a case we should log at INFO
or DEBUG
level? I'm not sure if that is something we should be flagging
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is common that some items are not in the fun_syms
, main
is the prime example (not sure about others, TBH)
fun_syms
(and the functions
table in the JSON) only contains functions that are called from within the program.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you add:
assert sym == 'main' or sym in fun_syms
Rather than this if
block, then run the tests? If it's just main
that's missing in our current test-suite, then we should probably keep the assertion so we get notified ASAP about that assumption breaking.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you find there are other entries missing, and it doesn't affect overall ability to build specs, then I guess it's fine to skip as is. If it's not common, but it still is something we should know about (because stable-mir-json
should be extracting more info), then I would do _LOGGER.warning(f'...')
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So, besides main
, we have two std::rt::lang_start...
functions and a drop_in_place
(for one of them) that are never in the function table, and one std::fmt::Debug
instance for &i32
(in two programs only).
whitelist = [
'main',
'std::rt::lang_start::<()>',
'<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once',
'std::ptr::drop_in_place::<{closure@std::rt::lang_start<()>::{closure#0}}>',
'<&i32 as std::fmt::Debug>::fmt',
]
assert sym in fun_syms or name in whitelist
The drop
function and the std::fmt::Debug
make me think we should keep the skipping code.
Custom drop
functions get called by the runtime (using a mechanism that we haven't investigated yet) and they can occur for many custom types in a program. Not sure what to think about the Debug
one
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We decided to leave the skipping code in place.
kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have one comment about changing the check to an assertion, we should probably fail as early as possible in cases we aren't sure what to do.
35a5092
to
f1edbb2
Compare
make_call_config
produces a configuration with aCall
terminator for the given start symbol in the K cell.Arguments to the function will be created as locals of a dummy caller's stack frame, and copied by
OperandCopy
in theCall
terminator.Arguments are symbolic values, with as much structure as the type metadata for the argument types allows.
Integer
, constraints limit the size of the value.struct
s andenum
s are created asAggregate
values but with a single variable (list-sorted) for the arguments. With more metadata for structs, we could create the struct fields with their resp. types.The dummy caller's locals have the following structure:
For sake of an example, ARG_2 here is a reference to data that was (symbolically) created at location P_2, behind the locals that serve as arguments of the called function. When the called function's locals are set up, the reference in
ARG_2
is copied and its offset adjusted to 1.