have the TermList default constructor zero-initialise

[MichaelRawson]

Somewhat trivial, but in discussion with @quickbeam123 have TermList zero-initialise its content. In (almost?) all cases this should be immediately overwritten, but it means that when there is a bug, we will get a hard null-dereference crash rather than...something else.

[joe-hauns]

Could we indstead of zero-initializing it initializing it in such a way that Term::isEmpty returns true?

[easychair]

I might be not up-to-date with the current code, but ... if the default initialization is ever used, would this not break term sharing? Or maybe in the future, if we decide that the default initialization can be legally used?

Andrei

On Thu, 28 Mar 2024 at 07:37, Joe Hauns @.***> wrote:

Could we indstead of zero-initializing it initializing it in such a way that Term::isEmpty returns true?

— Reply to this email directly, view it on GitHub https://github.com/vprover/vampire/pull/541#issuecomment-2024586102, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BMEASFYPQZ4LZIEMMDY2O3DNAVCNFSM6AAAAABFDKK2AWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMRUGU4DMMJQGI . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[MichaelRawson]

@joe-hauns - I had the same idea, but it seemed to me that an empty TermList should be a zero-initialised TermList. This doesn't work for some reason and crashes a lot - so I should figure out why, if two people want this.

@easychair - this is a good point. In principle it should not break term sharing, because we should never insert a Term containing an empty TermList into term sharing. But it would be smart to have some checks for this.

Either way - on hold for now until I look into it more, probably next week at this point.

[easychair]

There is a school of thought that says one should initialize memory which we are not supposed to access by rubbish that would almost certainly guarantee that accessing it will break the application.

null (0) is not rubbish

Of course, initializing by rubbish (even constant rubbish) may take a few microseconds and leave Vampire in second place in CASC :)

Cheers, Andrei

On Thu, 28 Mar 2024 at 13:51, Michael Rawson @.***> wrote:

@joe-hauns https://github.com/joe-hauns - I had the same idea, but it seemed to me that an empty TermList should be a zero-initialised TermList. This doesn't work for some reason and crashes a lot - so I should figure out why, if two people want this.

@easychair https://github.com/easychair - this is a good point. In principle it should not break term sharing, because we should never insert a Term containing an empty TermList into term sharing. But it would be smart to have some checks for this.

Either way - on hold for now until I look into it more, probably next week at this point.

— Reply to this email directly, view it on GitHub https://github.com/vprover/vampire/pull/541#issuecomment-2025236742, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BPFJF6Q2OCCEDQKAITY2QG5PAVCNFSM6AAAAABFDKK2AWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMRVGIZTMNZUGI . You are receiving this because you were mentioned.Message ID: @.***>

[MichaelRawson]

Could we indstead of zero-initializing it initializing it in such a way that Term::isEmpty returns true?

Done. :-) I've also added an assertion to TermSharing to make sure we don't inadvertently break that.

I did briefly try to have two categories of "empty" TermLists: the current one and a zero TermList, but Vampire uses both "invalid TermList" and "off the end of an argument list" somewhat blurrily so that wasn't workable.

[MichaelRawson]

See #384 - we no longer have "very special" variables, so SPEC_UPPER_BOUND is pointless. Also remove this here as I'm passing. Checking whether something is a special variable should now be very slightly faster.

[quickbeam123]

It's probably the SPEC_UPPER_BOUND test gone, which have us 3 ott problems and 5 discount10 TPTP problems solved extra with this, under -i 10000.