Frontc.parse_standalone_exp doesn't handle typedef-s

[sim642]

PR #97 exposed this functionality for Goblint to parse invariant expressions from witnesses:

cil/src/frontc/frontc.ml

Lines 273 to 282 in c7ffc37

	let parse_standalone_exp s =
	try
	if !E.verboseFlag then ignore (E.log "Frontc is parsing string: %s\n" s);
	flush !E.logChannel;
	(* if !E.verboseFlag then ignore @@ Parsing.set_trace true; *)
	let lexbuf = Clexer.initFromString s in
	let (cabs, _) = Stats.time "parse" (Cparser.expression (Whitetrack.wraplexer clexer)) lexbuf in
	Whitetrack.setFinalWhite (Clexer.get_white ());
	Clexer.finish ();
	cabs

This produces a parsing error when the expression contains a cast to a typedef-ed type. It is because of the ✨lexer hack✨ which makes the lexer stateful, even though parse_standalone_exp just seems to take a string and parse it to Cabs. Currently only the Cabs2cil process for such standalone expression requires some environment information (e.g. global variables, various type declarations) as argument.

However, due to the lexer hack, lexing of an identifier depends on knowing whether it is a variable name or a type name. Since parse_standalone_exp doesn't do anything about it, the lexer hack table isn't appropriately initialized and the lexer assumes everything to be a variable name. But variable names are not valid syntax in the cast type.

I'm not sure if we can really do anything about this because the lexer hack is a mutable hashtable during the parsing process. We have no way of restoring the state of this hashtable for any location required for invariant parsing. Unless the mutable hashtable is replaced with some persistent data structure that efficiently records the lexer hack table for all program points and allows us to time/location travel within it.
This is surprisingly complex and I'm not sure how, if at all, anyone else in SV-COMP manages to do this correctly.

[michael-schwarz]

At least for our own witnesses, we can remidy this to some extent by fullying unrolling all type expressions in casts when we generate them.