Stream: t-compiler/const-eval

Topic: Add symbolic execution to miri


Christian Poveda (Jun 26 2019 at 03:51, on Zulip):

Hi @oli, @eddyb. I'd like to start checking which parts of https://github.com/christianpoveda/sire can be properly integrated into miri. An small abstract of Oliver's first thoughts on the matter is here https://github.com/christianpoveda/sire/issues/1

RalfJ (Jun 26 2019 at 07:19, on Zulip):

Interesting project!

RalfJ (Jun 26 2019 at 07:20, on Zulip):

I think at some point we have to decide how much extra "messiness" we are willing to tolerate in CTFE/Miri for a case like this. Extra code complexity means higher maintanance cost and, worse, more bugs, so that's something I am quite concerned about.

RalfJ (Jun 26 2019 at 07:20, on Zulip):

There's a reason I keep refactoring things in the Miri engine ;)

Christian Poveda (Jun 26 2019 at 13:59, on Zulip):

Interesting project!

Thank you :)

I think at some point we have to decide how much extra "messiness" we are willing to tolerate in CTFE/Miri for a case like this. Extra code complexity means higher maintanance cost and, worse, more bugs, so that's something I am quite concerned about.

Well If i understand correctly, other than an additional associated type inside Machine, none of this wouldn't affect the rustcor miri repositories

oli (Jun 26 2019 at 14:02, on Zulip):

there'll probably be some additional hooks that we'll need to add to the Machine

oli (Jun 26 2019 at 14:02, on Zulip):

in miri and const eval these would be nops because their argument would be !

Christian Poveda (Jun 26 2019 at 14:04, on Zulip):

there'll probably be some additional hooks that we'll need to add to the Machine

Why?

oli (Jun 26 2019 at 14:05, on Zulip):

the logic for running operators on symbols needs to live somewhere

Christian Poveda (Jun 26 2019 at 14:06, on Zulip):

the logic for running operators on symbols needs to live somewhere

Well we could let that in other repo until this is actually used for something

Christian Poveda (Jun 26 2019 at 14:12, on Zulip):

Shouldn't the current methods of Machine be enough?

oli (Jun 26 2019 at 14:12, on Zulip):

not sure :D

oli (Jun 26 2019 at 14:12, on Zulip):

they have reached a point of complexity where I don't remember what's in there

Christian Poveda (Jun 26 2019 at 14:13, on Zulip):

Hahaha, I'm going to check the trait

Christian Poveda (Jun 26 2019 at 14:22, on Zulip):

Well it has more than we need. I did the first interpreter by immitating how miri executed code.

Christian Poveda (Jun 26 2019 at 14:27, on Zulip):

I guess we will discover what else Machine needs on the way

RalfJ (Jun 26 2019 at 20:21, on Zulip):

they have reached a point of complexity where I don't remember what's in there

:(

Christian Poveda (Jun 26 2019 at 20:29, on Zulip):

I'm going to start working on this on local to see what else do we need

RalfJ (Jun 26 2019 at 20:30, on Zulip):

there's also still some work left for intptrcast :D

RalfJ (Jun 26 2019 at 20:30, on Zulip):

like, making sure that &x as *const _ as usize actually does a cast

RalfJ (Jun 26 2019 at 20:30, on Zulip):

or what about a test that tries to print the address of a pointer?

Christian Poveda (Jun 26 2019 at 20:31, on Zulip):

Well, what about this. I'll work on intptrcast while you are awake and on this when you are not

RalfJ (Jun 26 2019 at 20:32, on Zulip):

;)

RalfJ (Jun 26 2019 at 20:32, on Zulip):

if you add "while I am awake and have time" there's not much time left :(

RalfJ (Jun 26 2019 at 20:32, on Zulip):

important paper deadline coming up

Christian Poveda (Jun 26 2019 at 20:32, on Zulip):

oh cool, where are you sending it?

RalfJ (Jun 26 2019 at 20:33, on Zulip):

but as long as we keep the intptrcast issue open so that this is still tracked, the current WIP implementation is a good start

RalfJ (Jun 26 2019 at 20:33, on Zulip):

oh cool, where are you sending it?

https://popl20.sigplan.org/

Christian Poveda (Jun 26 2019 at 20:33, on Zulip):

I had a lot of fun reading the last one

Christian Poveda (Jun 26 2019 at 20:35, on Zulip):

had fun = learned something

RalfJ (Jun 26 2019 at 20:46, on Zulip):

:)

Christian Poveda (Jun 26 2019 at 20:47, on Zulip):

like, making sure that &x as *const _ as usize actually does a cast

How are X as Y casts handled inside miri?

RalfJ (Jun 26 2019 at 20:50, on Zulip):

they are in librustc_mir/interpret/cast.rs

Christian Poveda (Jun 27 2019 at 16:03, on Zulip):

@oli there is a problem with adding the generic parameter to Operand

Christian Poveda (Jun 27 2019 at 16:03, on Zulip):

! does not implement the serialize traits :P

oli (Jun 27 2019 at 16:04, on Zulip):

hmm... implement it? :D

Christian Poveda (Jun 27 2019 at 16:05, on Zulip):

for real?

oli (Jun 27 2019 at 16:05, on Zulip):

I mean the serialization part is just match self {}

oli (Jun 27 2019 at 16:05, on Zulip):

and the deserialization is bug!()

Christian Poveda (Jun 27 2019 at 16:05, on Zulip):

I suppose that trying to serialize ! should fail

oli (Jun 27 2019 at 16:05, on Zulip):

nope

oli (Jun 27 2019 at 16:05, on Zulip):

that's dead code

Christian Poveda (Jun 27 2019 at 16:06, on Zulip):

what do you mean?

oli (Jun 27 2019 at 16:06, on Zulip):

you can't serialize a ! because there are no values of that type

Christian Poveda (Jun 27 2019 at 16:06, on Zulip):

yeah but what should the implementation do?

oli (Jun 27 2019 at 16:06, on Zulip):

match self {}

Christian Poveda (Jun 27 2019 at 16:06, on Zulip):

oh

Christian Poveda (Jun 27 2019 at 16:06, on Zulip):

duh

oli (Jun 27 2019 at 16:06, on Zulip):

:D

Christian Poveda (Jun 27 2019 at 16:06, on Zulip):

didn't get it the first time sorry

oli (Jun 27 2019 at 16:07, on Zulip):

it's a weird thing, because ! is essentially enum Void {}

Christian Poveda (Jun 27 2019 at 16:12, on Zulip):

bug! is not available inside serialize should i add rustc as a dependency? or use something else?

oli (Jun 27 2019 at 16:30, on Zulip):

just do unreachable!() then

Christian Poveda (Jun 27 2019 at 16:30, on Zulip):

great

Christian Poveda (Jun 27 2019 at 16:30, on Zulip):

did that :P

oli (Jun 27 2019 at 16:30, on Zulip):

heh

Christian Poveda (Jun 27 2019 at 16:30, on Zulip):

I'm having some trouble with the trait bounds

Christian Poveda (Jun 27 2019 at 16:32, on Zulip):

When trying to implement Debug for Operand<'tcx, T> where T is bounded to implement all the required traits (including Debug), compilation fails telling me that none of the traits are implemented for T

Christian Poveda (Jun 27 2019 at 16:33, on Zulip):
error[E0277]: can't compare `T` with `T`
    --> src/librustc/mir/mod.rs:2325:15
     |
2325 | impl<'tcx, T> Debug for Operand<'tcx, T> {
     |               ^^^^^ no implementation for `T == T`
     |
     = help: the trait `std::cmp::PartialEq` is not implemented for `T`
     = help: consider adding a `where T: std::cmp::PartialEq` bound
note: required by `mir::Operand`
    --> src/librustc/mir/mod.rs:2304:1
     |
2304 | pub enum Operand<'tcx, T = ()> where T: Clone + PartialEq + serialize::Encodable + serialize::Decodable {
     | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
oli (Jun 27 2019 at 16:34, on Zulip):

use impl<'tcx, T: Debug> I think?

oli (Jun 27 2019 at 16:34, on Zulip):

wait huh? PartialEq?

oli (Jun 27 2019 at 16:35, on Zulip):

oh

Christian Poveda (Jun 27 2019 at 16:35, on Zulip):

use impl<'tcx, T: Debug> I think?

Yeah but why the compiler complains on the type definition and not in the impl block?

oli (Jun 27 2019 at 16:35, on Zulip):

you may have to repeat all bounds on the type

oli (Jun 27 2019 at 16:35, on Zulip):

it tells you it's required by the definition

oli (Jun 27 2019 at 16:35, on Zulip):

not erroring on the definition

Christian Poveda (Jun 27 2019 at 16:35, on Zulip):

you may have to repeat all bounds on the type

Oohhhhhh

Christian Poveda (Jun 27 2019 at 16:35, on Zulip):

got it

Christian Poveda (Jun 27 2019 at 16:35, on Zulip):

my bad

oli (Jun 27 2019 at 16:35, on Zulip):

repeat all bounds from the type on the impl

oli (Jun 27 2019 at 16:36, on Zulip):

the former statement may have been ambiguous

Christian Poveda (Jun 27 2019 at 16:36, on Zulip):

yeah yeah got it

Christian Poveda (Jun 27 2019 at 16:37, on Zulip):

I don't know why I was expecting that the compiler would infer that T has the bounds that are imposed in the Operand definition.

oli (Jun 27 2019 at 16:38, on Zulip):

well... you're not wrong in that assumption, there's a bunch of talk about that topic

Christian Poveda (Jun 27 2019 at 16:38, on Zulip):

that sounds like a nasty discussion TBH

Christian Poveda (Jun 27 2019 at 16:39, on Zulip):

sometimes implicitness produces misunderstandings, I understand why this does not happen.

Christian Poveda (Jun 27 2019 at 16:44, on Zulip):

carrying all that trait bounds around the implementation seems cumbersome

Christian Poveda (Jun 27 2019 at 16:45, on Zulip):

I mean, I know why those are there, but It might look confusing to other people

Christian Poveda (Jun 27 2019 at 16:46, on Zulip):

Maybe there should be a supertrait for this?

oli (Jun 27 2019 at 17:01, on Zulip):

trait alias if anything

oli (Jun 27 2019 at 17:02, on Zulip):

but I also don't know why the type has those bounds

oli (Jun 27 2019 at 17:02, on Zulip):

instead of just the appropriate impls

oli (Jun 27 2019 at 17:02, on Zulip):

maybe fallout from some bound inference issues we used to have

oli (Jun 27 2019 at 17:02, on Zulip):

maybe open an issue?

oli (Jun 27 2019 at 17:02, on Zulip):

(sorry, "open an issue" is my go-to thing right now since there's no point in me looking at anything for the next weeks)

Christian Poveda (Jun 27 2019 at 18:15, on Zulip):

Sure no prob

Christian Poveda (Jun 27 2019 at 18:16, on Zulip):

This is just my side project while Ralf is busy/sleeping

RalfJ (Jun 27 2019 at 18:18, on Zulip):

more like melting, and hallucinating due to sleep deprivation^^

Christian Poveda (Jun 27 2019 at 18:18, on Zulip):

Anyway, I think I'll do an small list of what to do with the traits implemented by Operand in this case

Christian Poveda (Jun 27 2019 at 18:19, on Zulip):

more like melting, and hallucinating due to sleep deprivation^^

Nice way of making me to think twice about getting a PhD :P

Christian Poveda (Jun 27 2019 at 18:20, on Zulip):

Anyway, I think I'll do an small list of what to do with the traits implemented by Operand in this case

I don't know what is the proper place to do this, tecnically this is compiler code but is more related to miri, opening in the sire repo won't get enough visibility though.

RalfJ (Jun 27 2019 at 18:22, on Zulip):

Nice way of making me to think twice about getting a PhD :P

it's mostly unrelated to my PhD and mostly related to it being >35°C for the 4th day in a row, and my apartment being below the roof, so I have interior temperatures of >30°C, which is too hot to sleep...

RalfJ (Jun 27 2019 at 18:23, on Zulip):

(and I'm also not really hallucinating. but I am sleep deprived.)

Christian Poveda (Jun 27 2019 at 18:23, on Zulip):

Oh I was thinking about this in a more abstract sense heheh

Christian Poveda (Jun 27 2019 at 21:07, on Zulip):

I have an irrelevant but relevant question, which one is better? Operand::Atom or Operand::Symbol? @RalfJ has strong opinions on names so I'd like his opinion on this one

RalfJ (Jun 27 2019 at 21:37, on Zulip):

@Christian Poveda some context would be nice :D what are the origins of these names?

RalfJ (Jun 27 2019 at 21:37, on Zulip):

and what about Operand::Symbolic?

Christian Poveda (Jun 27 2019 at 21:41, on Zulip):

So basically we want an operand variant to store symbols during symbolic execution

Christian Poveda (Jun 27 2019 at 21:42, on Zulip):

the idea is to use the MIR of a function as the instructions to propagate symbols representing the functions argument

Christian Poveda (Jun 27 2019 at 21:44, on Zulip):

and this Operand::FancySymbolName is the representation of such symbols

RalfJ (Jun 27 2019 at 21:46, on Zulip):

but won't this, in general, also be something like x + 2? Why should it always be an "atom"?

RalfJ (Jun 27 2019 at 21:46, on Zulip):

like, after fn foo(x: i32) { let y = x+2; ... }

Christian Poveda (Jun 27 2019 at 21:47, on Zulip):

yes that is true

Christian Poveda (Jun 27 2019 at 21:47, on Zulip):

it was just because Symbol is already used inside rustc for something else, so the next word that came to my head was Atom

Christian Poveda (Jun 27 2019 at 21:49, on Zulip):

so Operand::Symbolic it is?

RalfJ (Jun 27 2019 at 22:12, on Zulip):

so Operand::Symbolic it is?

seems good to me

Christian Poveda (Jun 27 2019 at 22:13, on Zulip):

ok it seems I did not broke miri nor the compiler :D

RalfJ (Jun 27 2019 at 22:15, on Zulip):

always a good start :D

Christian Poveda (Jun 28 2019 at 00:37, on Zulip):

I did a PR with the new variant, it shouldn't be groundbreaking but I'll help me to get started working independently

oli (Jun 28 2019 at 06:47, on Zulip):

Oh no :smiley: you picked the wrong Operand type

Christian Poveda (Jun 28 2019 at 06:47, on Zulip):

Oh no :smiley: you picked the wrong Operand typr

Was?

Christian Poveda (Jun 28 2019 at 06:47, on Zulip):

Es gibt andere Operand?

oli (Jun 28 2019 at 06:47, on Zulip):

Jop

Christian Poveda (Jun 28 2019 at 06:48, on Zulip):

ELI5 please

oli (Jun 28 2019 at 06:48, on Zulip):

The miri engine has one

oli (Jun 28 2019 at 06:48, on Zulip):

In operand.rs

Christian Poveda (Jun 28 2019 at 06:49, on Zulip):

Ohhh the one with the Immediates

oli (Jun 28 2019 at 06:49, on Zulip):

The MIR one doesn't need to know about symbolic

Christian Poveda (Jun 28 2019 at 06:49, on Zulip):

got it

oli (Jun 28 2019 at 06:50, on Zulip):

Oops, sorry I should have checked when you first linked me to stuff

oli (Jun 28 2019 at 06:51, on Zulip):

In order to be able to use it in sire you'll need to also add the generic parameter to OpTy and as an associated type to the machine I believe

Christian Poveda (Jun 28 2019 at 06:51, on Zulip):

ok let me "undo" this

oli (Jun 28 2019 at 06:52, on Zulip):

Hehe what would we do without git

oli (Jun 28 2019 at 06:52, on Zulip):

How do ppl still use svn or dated folder copies... oh off topic rant

Christian Poveda (Jun 28 2019 at 06:53, on Zulip):

I knew of a company that used DROPBOX!

oli (Jun 28 2019 at 06:53, on Zulip):

And they probably thought they were modern because cloud and stuff

Christian Poveda (Jun 28 2019 at 06:54, on Zulip):

well they did web applications so they used everything that had hype, could you imagine dropbox syncing the node_modules folder?

oli (Jun 28 2019 at 06:55, on Zulip):

I think if you make the Frame's locals array use of OpTy generic over the Machine associated type for the symbols, the compiler should tell you all the other places that need changing

oli (Jun 28 2019 at 06:55, on Zulip):

I'm not sure I want to know more, I have a nightmare free sleep and want to keep it

Christian Poveda (Jun 28 2019 at 06:56, on Zulip):

I'm not sure I want to know more, I have a nightmare free sleep and want to keep it

Sorry for ruining your holiday

Christian Poveda (Jun 28 2019 at 06:57, on Zulip):

I'm going to add the parameter to the Operand type first and see what's up there

oli (Jun 28 2019 at 06:57, on Zulip):

Still working today

Christian Poveda (Jun 28 2019 at 06:59, on Zulip):

I don't want to check my work email, there is stuff in that inbox that makes the dropbox think look ok in comparison

Christian Poveda (Jun 28 2019 at 07:00, on Zulip):

Ohh, it is ok to default the associated type inside Machine to never also?

Christian Poveda (Jun 28 2019 at 07:00, on Zulip):

Because default assoc types are unstable IIRC

oli (Jun 28 2019 at 07:00, on Zulip):

Yes

oli (Jun 28 2019 at 07:00, on Zulip):

Oh

oli (Jun 28 2019 at 07:01, on Zulip):

Maybe don't do it then

oli (Jun 28 2019 at 07:01, on Zulip):

Just make miri and const eval use !

Christian Poveda (Jun 28 2019 at 07:01, on Zulip):

Will do

oli (Jun 28 2019 at 07:01, on Zulip):

Defaulted assoc types are problematic

oli (Jun 28 2019 at 07:01, on Zulip):

I keep forgetting

Christian Poveda (Jun 28 2019 at 07:01, on Zulip):

how so?

oli (Jun 28 2019 at 07:02, on Zulip):

Iirc they cause defaulted method bodies to disappear if you have a custom type for the defaulted assoc type

oli (Jun 28 2019 at 07:03, on Zulip):

So sire would have to impl all machine methods

oli (Jun 28 2019 at 07:03, on Zulip):

Oh tbh it probably has to do that anyway

oli (Jun 28 2019 at 07:04, on Zulip):

But it's not the end of the world to have miri break and make it add an assoc type

Christian Poveda (Jun 28 2019 at 07:06, on Zulip):

:P

Christian Poveda (Jun 28 2019 at 07:06, on Zulip):

do you have any kewl names for the assoc type inside machine?

Christian Poveda (Jun 28 2019 at 07:06, on Zulip):

SymbolicSymbol?

oli (Jun 28 2019 at 07:10, on Zulip):

XD why not just Symbolic?

Christian Poveda (Jun 28 2019 at 07:12, on Zulip):

/me invokes @RalfJ for naming conventions

Christian Poveda (Jun 28 2019 at 07:25, on Zulip):

Maybe will do the assoc type in Machine in a different PR, because that one is going to break miri for sure :P

RalfJ (Jun 28 2019 at 07:54, on Zulip):

SymbolicValue? SymbolicOperand? Symbol? Not sure^^

Christian Poveda (Jun 28 2019 at 07:56, on Zulip):

Ok the PR for Operand is ready, it does not break any tests (including miri)

oli (Jun 28 2019 at 09:16, on Zulip):

@Christian Poveda oh you want to just do the OpTy and Operand changes and start using these in sire?

oli (Jun 28 2019 at 09:17, on Zulip):

without resorting to using an InterpCx yet

Christian Poveda (Jun 28 2019 at 12:32, on Zulip):

Yeah I still need to start migrating the machine methods

Christian Poveda (Jun 28 2019 at 12:32, on Zulip):

I think I can tape up everything Else if I need to

Christian Poveda (Jun 28 2019 at 14:01, on Zulip):

patch with tape*

Christian Poveda (Jul 22 2019 at 16:04, on Zulip):

Should I continue this or should we let this for lateR?

Christian Poveda (Jul 22 2019 at 16:04, on Zulip):

I tried to access the PR on github but the site is returning a 500 error :P

Last update: Nov 15 2019 at 21:10UTC