From 6310b9c7e255d78a04fc0d3d28b85738b1c4a077 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 20 Sep 2021 10:16:33 -0400 Subject: [PATCH 1/2] Impose lower version bounds on config-schema Fixes #852. --- crux-llvm/crux-llvm.cabal | 2 +- crux/crux.cabal | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal index 73d93aa94..e16806be6 100644 --- a/crux-llvm/crux-llvm.cabal +++ b/crux-llvm/crux-llvm.cabal @@ -89,7 +89,7 @@ library build-depends: aeson, bv-sized, - config-schema, + config-schema >= 1.2.2.0, data-binary-ieee754, logict, llvm-pretty, diff --git a/crux/crux.cabal b/crux/crux.cabal index fbe372c3d..ae430cdd3 100644 --- a/crux/crux.cabal +++ b/crux/crux.cabal @@ -54,7 +54,7 @@ library raw-strings-qq, simple-get-opt, config-value, - config-schema, + config-schema >= 1.2.2.0, semigroupoids, unordered-containers, xml, From b6c188128c27647e611afd77c612336a2a682e0d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 20 Sep 2021 10:21:36 -0400 Subject: [PATCH 2/2] crux-llvm: Add some missing __VERIFIER_nondet_* overrides This adds `crux-llvm` overrides for the `u8`, `u16`, `u32`, `unsigned`, `size_t`, `loff_t`, and `longlong` variants of `__VERIFIER_nondet_*`. This checks off several boxes in #842. --- crux-llvm/src/Crux/LLVM/Overrides.hs | 33 ++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs index d115973da..256703fa9 100644 --- a/crux-llvm/src/Crux/LLVM/Overrides.hs +++ b/crux-llvm/src/Crux/LLVM/Overrides.hs @@ -251,6 +251,19 @@ svCompOverrides :: [OverrideTemplate (personality sym) sym arch rtp l a] svCompOverrides = [ basic_llvm_override $ + [llvmOvr| i64 @__VERIFIER_nondet_longlong() |] + (sv_comp_fresh_bits (knownNat @64)) + + -- loff_t is pretty Linux-specific, so we can't point to the C or POSIX + -- standards for justification about what size it should be. The man page + -- for lseek64 (https://linux.die.net/man/3/lseek64) is as close to a + -- definitive reference for this as I can find, which says + -- "The type loff_t is a 64-bit signed type". + , basic_llvm_override $ + [llvmOvr| i64 @__VERIFIER_nondet_loff_t() |] + (sv_comp_fresh_bits (knownNat @64)) + + , basic_llvm_override $ [llvmOvr| size_t @__VERIFIER_nondet_ulong() |] (sv_comp_fresh_bits ?ptrWidth) @@ -258,6 +271,14 @@ svCompOverrides = [llvmOvr| size_t @__VERIFIER_nondet_long() |] (sv_comp_fresh_bits ?ptrWidth) + , basic_llvm_override $ + [llvmOvr| i32 @__VERIFIER_nondet_unsigned() |] + (sv_comp_fresh_bits (knownNat @32)) + + , basic_llvm_override $ + [llvmOvr| i32 @__VERIFIER_nondet_u32() |] + (sv_comp_fresh_bits (knownNat @32)) + , basic_llvm_override $ [llvmOvr| i32 @__VERIFIER_nondet_uint() |] (sv_comp_fresh_bits (knownNat @32)) @@ -266,6 +287,10 @@ svCompOverrides = [llvmOvr| i32 @__VERIFIER_nondet_int() |] (sv_comp_fresh_bits (knownNat @32)) + , basic_llvm_override $ + [llvmOvr| i16 @__VERIFIER_nondet_u16() |] + (sv_comp_fresh_bits (knownNat @16)) + , basic_llvm_override $ [llvmOvr| i16 @__VERIFIER_nondet_ushort() |] (sv_comp_fresh_bits (knownNat @16)) @@ -274,6 +299,10 @@ svCompOverrides = [llvmOvr| i16 @__VERIFIER_nondet_short() |] (sv_comp_fresh_bits (knownNat @16)) + , basic_llvm_override $ + [llvmOvr| i8 @__VERIFIER_nondet_u8() |] + (sv_comp_fresh_bits (knownNat @8)) + , basic_llvm_override $ [llvmOvr| i8 @__VERIFIER_nondet_uchar() |] (sv_comp_fresh_bits (knownNat @8)) @@ -286,6 +315,10 @@ svCompOverrides = [llvmOvr| i1 @__VERIFIER_nondet_bool() |] (sv_comp_fresh_bits (knownNat @1)) + , basic_llvm_override $ + [llvmOvr| size_t @__VERIFIER_nondet_size_t() |] + (sv_comp_fresh_bits ?ptrWidth) + , basic_llvm_override $ [llvmOvr| float @__VERIFIER_nondet_float() |] (sv_comp_fresh_float SingleFloatRepr)