This project is read-only.

Why does memory reinterpretation destroy ghost fields?

Jun 7, 2010 at 12:38 PM
Edited Jun 7, 2010 at 12:56 PM

Dear all,

while I understand that memory reinterpretation destroys implementation fields, it also destroys ghost fields:

#include "vcc.h"

typedef struct A_str {

    unsigned int real;
    spec(unsigned int ^ghost;) 

} A_t;

void test (A_t *a) 
requires(a->ghost == 0)

    assert(a->ghost == 0); 
    from_bytes(a, false);
    assert(a->ghost == 0);  //<-- fails



Verification of test [2,67s] failed.
p:\tool\vcc\sandbox\memory\from_bytes_ghost.c(24,14) : error VC9500: Assertion 'a->ghost == 0' did not verify.
Time: 4,71s total, 1,98s compiler, 0,00s Boogie, 2,72s method verification.
Detected verification errors in 1 methods.
Exiting with 3 (1 error(s).)

 Is this is (desirable/necessary?) feature or something that could be changed? Rationale is that I prefer to store the specification as close to the implementation as possible and not discarding ghost state during memory reinterpretation also seems to be a logical concept to me.

Or is there any trick/switch to change the default behavior?

Thanks for insights, Holger 

Jun 7, 2010 at 6:27 PM

You’re right: destroying ghost data is unnecessary.

I’ve a patch to fix it, but be advised that it only works locally – the to/from_bytes won’t destroy the information about ghost fields, but because they become untyped, any call will lose that information. Normally, you can use the domains to prevent that, but not for untyped data. Is that OK for you?


Jun 7, 2010 at 8:52 PM
Hi Michal, thanks for the offer. To avoid any misunderstanding here: you mean that if your patch were applied and in the above example I had used typedef struct A_str { unsigned int real; spec(obj_t o;) invariant(keeps(o)) } A_t; (that is "obj_t o" replacing "unsigned int ^ghost") this still (1) would incur information loss after the first call or (2) in this setup the information bound to the object o could be still salvaged after a subsequent call by using an "assert(in_domain(a->o, a))"? Generally, speaking from what I would consider most intuitive from a user point of view is that to/from_bytes won't destroy neither "data" nor typing information of ghost fields (my understanding is that as of now they already preserve the is_object_root property which is also some kind of specification state) - I imagine these to work on the naked implementation state (both its "data" and typing) only. If asking for this messes up the implementation and/or theory that of course would be a strong counter-argument and even the less powerful patch of only local availability might be useful (that's something I would have to spend more thinking/testing on ...).
Jun 10, 2010 at 6:21 AM

(1) Yes, but note that wrap/unwrap/from/to_bytes don’t count as calls.

(2) Yes.

We have an axiom saying typed(p)->typed(emb(p)), which wouldn’t work for ghost fields. This axiom seems needed in our current axiomatization, but is gone in the new prelude (vcc3), which I’ll be working on this summer. But this is likely 3-4 month timeframe, and pretty sure loss of complete backward compatibility.

As a workaround, you can always use something like (in mixture of new and old syntax):

\state s = \current_state();




o->f1 = \at(s, o->f1);

o->f2 = \at(s, o->f2);


Additionally, you can combine several ghost fields into a record.