Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Bug in Cil.datatype.Lval.Hashtbl?

Hi,

On Tue, Aug 7, 2012 at 9:30 AM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:
> I read the line "Note that the equality is based on eid (for
> sub-expressions).", but I didn't tell me much. Does eid refer to
> Cil_types.exp.eid?

Yes.

> If so, what happens if the lhost is a varinfo (which doesn't have a field eid)?

Then comparison and hash will "succeed", for your definition of
success. However, see below.

> if(cond) this->gear++;
> else this->gear--;
>
> I don't see why this->gear should be considered being different here and I
> don't yet understand why I get different hash values.

As 'this' is a pointer, this->gear is represented internally as

Mem ({ enode = Var vthis; ...}, Field (fgear, NoOffset))

The first argument of the Mem constructor is an expression. Thus, your
two occurrences of this->gear will contain two different
Cil_types.exp, that will have two different eids. The two lvals will
hash to two different values, and will also compare differently.


On a broader note : comparison and hash functions for a datatype are
expected to verify a few properties. Amongst them are
(1) equality according to the equality function imply equal hashes ;
otherwise, hash tables will misbehave
(2) if possible, computation must be fast ; standard complexity
analyses on datastructures such as balanced trees or hash tables
suppose that those operation can be done in O(1)

The hash function on terms in Nitrogen was buggy, because (1) was not
verified. This was fixed during the development of Oxygen. Moreover,
the new hash function will run in O(1) (albeit with possibly a big
constant). Equality and comparisons were and will remain in O(n).

For expressions, speed was important and we added the eid fields ;
this is sufficient to guarantee a O(1) computation time for equality,
comparison and hash, with a very low constant. As a result, those
operations are also quite efficient on lvals. The disadvantage is that
equality now becomes "same syntactic occurrence", instead of "same
expression/lval". As Virgile pointed out, the notion of equality you
want is given by the functions Cil.compareExp and Cil.compareLval, but
it is not available as comparison or hash functions. A patch that
implement this functionality, by mirroring what
compareExp/compareLval/compareOffset do, would be welcome.

Hope this helps,

-- 
Boris