sosy-lab/sv-witnesses

Linter crashes on seemingly valid witness

danieldietsch opened this issue · 1 comments

Version 1.0 b4c8a12 of the linter crashes for the attached witness and file with

$ witnesslinter.py --ignoreSelfLoops --witness witness.graphml sv-benchmarks/c/pthread-wmm/mix014_power.oepc.i
CRITICAL: line 658: Malformed witness:
        xmlSAX2Characters, line 658, column 1

witnesslint finished with exit code 1
free(): double free detected in tcache 2
Aborted

witness.graphml.txt
mix014_power.oepc.i.txt

This is caused by a crash of the lxml parser used internally. There is nothing wrong with the witness, this crash can happen for arbitrary witnesses for the following reason:

In order to save memory we remove parsed nodes once they have been processed via parent_elem.remove(elem). However, the lxml docs clearly state (cf. here)

you must not modify or move the ancestors (parents) of the current element. You should also avoid moving or discarding the element itself

as this can cause unexpected behavior.

e9704ca replaces the problematic lines with elem.clear() calls which are allowed. These remove unnecessary information but keep the element itself. This way the linter will need more memory, but afaik there haven't been any cases yet where the linter ran out of memory anyway and testing with a > 500 MB witness has shown no problems.