GitLab

Submitted by Johannes Kanig

Submitted by Johannes Kanig

lskept: the old selection check required at least one non-variable
non-closed type in the lsymbol's signature. This is too permissive,
because (list_match : list 'a -> 'b -> 'b) is allowed and will produce
an instance for every type in the "inst" set. The new check requires
that all freely standing type variables occur under a type constructor
elsewhere in the lsymbol's signature.

lsinst: accept any monomorphic instance of any polymorphic symbol
except equality. The old procedure applied the same restrictions
as for the "lskept" set which serve no real purpose for "lsinst".

Best of three runs on a bench for Gappa transformations:
- before: 34.98user 0.09system 0:35.13elapsed 99%CPU (0avgtext+0avgdata 241492maxresident)k
- after:  29.68user 0.08system 0:29.80elapsed 99%CPU (0avgtext+0avgdata 241820maxresident)k
Speed-up: +18%.

Sharing is caring, right?

this is useful to declare on-the-fly a new sort which replaces
a complex type. Otherwise, the printer has to traverse any term
twice: first, to detect complex types, second, to print the term.

also, avoid the "encoding_sort" transformation, if it can be done
directly in the printer.

On the same example as in the previous commits, this gives 5x
acceleration together with some memory usage reduction.

I didn't increment the version just for this fix, so sessions
are officially broken between the previous commit and this one.

feel free to revert, if you think we might want to make again the
distinction between t_equal and t_equal_alpha in future or just
don't feel like breaking the API.

also, ensure that t_label_copy does not lose information

the goal declarations are not shared and thus memoizing transformations
on them is only interesting if we apply the same transformation on the
same goal (which may happen when we launch several provers of the same
family on the same goal). On the other hand, goal declarations are big
(think WP) and numerous (think goal_split), and keeping them in memory
is a bad idea.

The same example from BWare can now be treated with 1/4 of memory:

why3-replayer : full memoization
106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k

why3-replayer : no memoization on goals (this commit)
74.14user 4.24system 1:24.93elapsed 92%CPU (0avgtext+0avgdata 429376maxresident)k

why3-replayer : no memoization at all
217.78user 6.25system 3:43.56elapsed 100%CPU (0avgtext+0avgdata 615204maxresident)k

One side effect of this commit is that polymorphism encoding
transformations are likely to be memoized only for a short time.
The transformations that select the type instances to discriminate
and the types to preserve in encoding are full-task-dependent and
therefore are not memoized anymore. Thus, as soon the the task that
contains all the selection metas is GCed, the rest of the chain
will go, too, and Why3 will have to re-monomorphize the same decls.
We'll see if this is a problem in practice.

The rationale for this change is that the major case of term duplication
is a transformation that changes only some parts of a term, leaving the
rest intact. This case can be handled with the help of Term.t_label_copy
(which must be called anyway, to preserve labels): if the two terms are
"similar", i.e. composed from the identical components, we return the
original and drop the copy. The duplication of unrelated terms is more
rare, because of bound variables which are mostly unique.

Decls and tasks are still h-consed, however, to permit memoization.

On the same example of BWare the gain is quite visible:

why3-replayer : hcons

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

why3-replayer : no hcons

106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k

we still keep bv_vars in the binders, so calculating the set
of free variables only has to descend to the topmost binders.
The difference on an example from BWare is quite striking:

/usr/bin/time why3-replayer : with t_vars

505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k

/usr/bin/time why3-replayer : without t_vars

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

Not only we take 2/3 of memory, but we also gain in speed (less work
for the GC, most probably).

This patch should be tested on big WhyML examples,
since src/whyml/mlw_*.ml are big users of t_vars.

Thanks to Guillaume for the suggestion.