SV-COMP: Add overrides for more __VERIFIER_nondet_* functions

[RyanGlScott]

Currently, crux-llvm has overrides for the following SV-COMP–related __VERIFIER_nondet_* functions:

crucible/crux-llvm/src/Crux/LLVM/Overrides.hs

Lines 249 to 296 in c96a404

	svCompOverrides ::
	(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
	[OverrideTemplate (personality sym) sym arch rtp l a]
	svCompOverrides =
	[ basic_llvm_override $
	[llvmOvr| size_t @__VERIFIER_nondet_ulong() |]
	(sv_comp_fresh_bits ?ptrWidth)
	, basic_llvm_override $
	[llvmOvr| size_t @__VERIFIER_nondet_long() |]
	(sv_comp_fresh_bits ?ptrWidth)
	, basic_llvm_override $
	[llvmOvr| i32 @__VERIFIER_nondet_uint() |]
	(sv_comp_fresh_bits (knownNat @32))
	, basic_llvm_override $
	[llvmOvr| i32 @__VERIFIER_nondet_int() |]
	(sv_comp_fresh_bits (knownNat @32))
	, basic_llvm_override $
	[llvmOvr| i16 @__VERIFIER_nondet_ushort() |]
	(sv_comp_fresh_bits (knownNat @16))
	, basic_llvm_override $
	[llvmOvr| i16 @__VERIFIER_nondet_short() |]
	(sv_comp_fresh_bits (knownNat @16))
	, basic_llvm_override $
	[llvmOvr| i8 @__VERIFIER_nondet_uchar() |]
	(sv_comp_fresh_bits (knownNat @8))
	, basic_llvm_override $
	[llvmOvr| i8 @__VERIFIER_nondet_char() |]
	(sv_comp_fresh_bits (knownNat @8))
	, basic_llvm_override $
	[llvmOvr| i1 @__VERIFIER_nondet_bool() |]
	(sv_comp_fresh_bits (knownNat @1))
	, basic_llvm_override $
	[llvmOvr| float @__VERIFIER_nondet_float() |]
	(sv_comp_fresh_float SingleFloatRepr)
	, basic_llvm_override $
	[llvmOvr| double @__VERIFIER_nondet_double() |]
	(sv_comp_fresh_float DoubleFloatRepr)
	]

This doesn't cover everything, however. Per the 2021 SV-COMP rules:

__VERIFIER_nondet_X(): In order to model nondeterministic values, the following functions can be assumed to return an arbitrary value of the indicated type: __VERIFIER_nondet_X() (and nondet_X(), deprecated) with X in {bool, char, int, float, double, loff_t, long, pchar, pthread_t, sector_t, short, size_t, u32, uchar, uint, ulong, unsigned, ushort} (no side effects, pointer for void *, etc.). The verification tool can assume that the functions are implemented according to the following template:
X __VERIFIER_nondet_X() { X val; return val; }

By my count, crux-llvm is missing overrides for the following __VERIFIER_nondet_* variants:

• loff_t
• pchar
• pthread_t
• sector_t
• size_t
• u32
• unsigned

I'm unclear if all of these are actually used in SV-COMP in practice, but I have spotted a subset of these in the wild:

• ldv-validator-v0.6/linux-stable-a9e7fb5-1-32_7a-drivers--media--rc--imon.ko-entry_point.cil.out.i uses __VERIFIER_nondet_loff_t.
• ldv-validator-v0.6/linux-stable-d47b389-1-32_7a-drivers--media--video--cx88--cx88-blackbird.ko-entry_point.cil.out.i uses __VERIFIER_nondet_size_t.
• ldv-validator-v0.6/linux-stable-431e8d4-1-102_1a-drivers--net--r8169.ko-entry_point.cil.out.i uses __VERIFIER_nondet_u32.

In addition to the ones above, I have spotted a number of __VERIFIER_nondet_* variants that aren't specified in the rules:

• ldv-commit-tester/main0_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa.i uses __VERIFIER_nondet_longlong.
• heap-data/packet_filter.i uses __VERIFIER_nondet_charp.
• ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--rtlwifi--btcoexist--btcoexist.ko-entry_point.cil.out.i uses __VERIFIER_nondet_u8.
• ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--intel--i40evf--i40evf.ko-entry_point.cil.out.i uses __VERIFIER_nondet_u16.
• ldv-commit-tester/main0_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa.i uses __VERIFIER_nondet_ulonglong.

I'm unclear if we should add support for these right away, as their inclusion in SV-COMP could arguably be considered a bug. I've submitted https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1304 in an attempt to clarify the situation. EDIT: See #842 (comment).

[robdockins]

Many of those seem uncomplicated.

The intended semantics of __VERIFIER_nondet_pchar seem pretty mysterious to me. Should the resulting pointer be valid? Should it point to allocated memory? How much? etc.

Not sure it makes sense for us to support pthread_t at this point, since we don't support any pthread overrides. Probably similar for sector_t, although I don't know exactly what API that goes with.

[RyanGlScott]

For what it's worth, many of these functions are only used in a small number of programs:

$ git grep -nl "__VERIFIER_nondet_pchar" .
c/ddv-machzwd/ddv_machzwd_all.i
c/ddv-machzwd/ddv_machzwd_inb.i
c/ddv-machzwd/ddv_machzwd_inb_p.i
c/ddv-machzwd/ddv_machzwd_inl.i
c/ddv-machzwd/ddv_machzwd_inl_p.i
c/ddv-machzwd/ddv_machzwd_inw.i
c/ddv-machzwd/ddv_machzwd_inw_p.i
c/ddv-machzwd/ddv_machzwd_outb.i
c/ddv-machzwd/ddv_machzwd_outb_p.i
c/ddv-machzwd/ddv_machzwd_outl.i
c/ddv-machzwd/ddv_machzwd_outl_p.i
c/ddv-machzwd/ddv_machzwd_outw_p.i
c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i

$ git grep -nl "__VERIFIER_nondet_pthread_t" .
c/ddv-machzwd/ddv_machzwd_all.i
c/ddv-machzwd/ddv_machzwd_inb.i
c/ddv-machzwd/ddv_machzwd_inb_p.i
c/ddv-machzwd/ddv_machzwd_inl.i
c/ddv-machzwd/ddv_machzwd_inl_p.i
c/ddv-machzwd/ddv_machzwd_inw.i
c/ddv-machzwd/ddv_machzwd_inw_p.i
c/ddv-machzwd/ddv_machzwd_outb.i
c/ddv-machzwd/ddv_machzwd_outb_p.i
c/ddv-machzwd/ddv_machzwd_outl.i
c/ddv-machzwd/ddv_machzwd_outl_p.i
c/ddv-machzwd/ddv_machzwd_outw_p.i
c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i

$ git grep -nl "__VERIFIER_nondet_sector_t" .
c/ddv-machzwd/ddv_machzwd_all.i
c/ddv-machzwd/ddv_machzwd_inb.i
c/ddv-machzwd/ddv_machzwd_inb_p.i
c/ddv-machzwd/ddv_machzwd_inl.i
c/ddv-machzwd/ddv_machzwd_inl_p.i
c/ddv-machzwd/ddv_machzwd_inw.i
c/ddv-machzwd/ddv_machzwd_inw_p.i
c/ddv-machzwd/ddv_machzwd_outb.i
c/ddv-machzwd/ddv_machzwd_outb_p.i
c/ddv-machzwd/ddv_machzwd_outl.i
c/ddv-machzwd/ddv_machzwd_outl_p.i
c/ddv-machzwd/ddv_machzwd_outw_p.i
c/ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.i

As a result, the answers to questions like "what are the intended semantics?" may very well be "whatever makes the programs in c/ddv-machzwd work". That being said, I think I agree that we should hold off on some of the weirder ones like pthread_t.

[RyanGlScott]

https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1304#note_693280508 clarifies that the omission of the longlong, u8 and u16 variants of __VERIFIER_nondet_* from the SV-COMP rules is an oversight, and that uses of __VERIFIER_nondet_charp in the benchmarks should eventually be removed due to its unclear semantics.