Baseline verifiers producing the wrong count for numFields during benchmarking

The BenchmarkExecutor calls SelectVisitor.visit on the IR generated with Main.generateIR (which is also what --dynamic uses); the --dynamic mode does not call SelectVisitor.visit, which makes sense as SelectVisitor is for generating different permutations of specs. SelectVisitor.visit calls super.visit which eventually calls SelectVisitor's collectOutput method, which returns the IR of the program after visiting it: it calls program.copy(this.methods.toList, this.predicates.toList) which takes the newly visited methods and predicates and creates a new program IR from them and the structs from program. However, it creates new struct objects in this process, so the old struct objects are referred to by fields in the methods and predicates and the struct list refers to new struct objects with the same contents. This causes the BaselineChecker's modification of the struct list in the IR to add _id to each struct to only apply to the struct list and not the structs referred to by fields in the methods and predicates. Of course, BaselineChecker uses those fields and their corresponding structs to calculate numFields resulting in a count without _id. Meanwhile, --dynamic mode, which doesn't modify the IR, has its fields referring to the same structs as in program.structs, so the same call to BaselineChecker works as intended and generates a numFields count including _id.

Gradual checking from BenchmarkExecutor relies on Checker rather than BaselineChecker and isn't affected by this issue because Checker uses the new struct objects to set the numFields entry rather than the old ones. So, I'm going to borrow the gradual code's method to fix the issue, since I'm sure .copy is probably used elsewhere where its current behavior is necessary.

I also am going to fix the count to not include _id generally for all checkers/verifiers, because including _id in the count makes run-time checking in runtime.c0/.h0 for ownedfields operate not as intended. However, there are some trade-offs here in terms of performance w.r.t to including _id in the count and the ownedfields implementation in runtime.c0:

if we include _id then technically we gain performance from not allocating arrays as frequently, buuut idk it's pretty negligible in the long run I think
eventually whenever we have examples that lose permissions then including _id would use more memory while not including _id would save on memory by deleting/overwriting unused arrays
we always add back in the removed perms eventually so we don't save on memory in our benchmarks currently

gradual-verification / gvc0

Baseline verifiers producing the wrong count for numFields during benchmarking #58