correctcomputation / checkedc-clang

This is the primary development repository for 3C, a tool for automatically converting legacy C code to the Checked C extension of C, which aims to enforce spatial memory safety. This repository is a fork of Checked C's.
14 stars 5 forks source link

Ensure every constraint to wild has its own PSL and remove the `AtomSourceMap`? #612

Open mattmccutchen-cci opened 3 years ago

mattmccutchen-cci commented 3 years ago

Currently, when 3C adds a constraint (including a constraint to wild), it can specify a PSL, which is supposed to identify the code that resulted in the constraint between the two atoms. When 3C reports a root cause of wildness, it uses the PSL of the constraint to wild if one is specified, otherwise it falls back to the AtomSourceMap, which is supposed to give the PSL of the definition of the program element that was constrained to wild. This fallback has pros and cons, though they each have caveats:

Mike said at yesterday's meeting that as we increasingly prioritize user-friendliess of 3C, we should commit to specifying a good PSL for every constraint to wildness and drop the AtomSourceMap fallback. I'm not completely convinced, but I'm going ahead and filing an issue for it.

kyleheadley commented 2 years ago

I ran into the AtomSourceMap when improving conflicting constrints in #708. Conflicts happen at an atom, and while that PR uses the neighboring constraints with their PSLs, it also references the atom itself, which doesn't have a PSL(it uses the default). This is improved in code that runs later by reading the AtomSourceMap.

So the map stores the PSLs for declarations, which can be just as useful for user-friendliness as the constraint generating locations.