Module Gc.Conservative

Conservative Garbage Collector.

This component implements a (very) conservative garbage collection algorithm, i.e., it may treat a lot of dead taints as live but will never collect a taint that is reachable.

The algorithm tracks only variables (registers and temporaries) and collects objects that are not stored in the heap and no longer reachable via the variables.

Taint is live if either of the following is true: 1. it is attached to a value of a variable in Env.all; 2. it is attached to any address.

The second clause gives a possibility for over-approximation, as we do not track, whether an address is reachable from the current program location. So once a tainted value is stored and the taint is attached to an address, the only way to kill this taint, is to overwrite it with another value using another store operation.

Currently, the garbage collection runs every machine instruction but this may change in future.