Support for symbolic strings #88

alastairreid · 2021-02-09T11:30:50Z

Composed of

Efficient support for creating symbolic Vec.
Tests involving strings
Creating a new top-level directory 'runtime' to contain C support code required to interface between what the Rust library expects from the C library and the set of operations provided by different verifiers.
- This will probably end up being a combination of code that is needed by all verifiers and code that is only needed with a subset of the verifier backends that we support. So it will end up requiring conditional compilation.
- For now all it contains is support for allocating aligned memory blocks (used by crates like Regex).
- In the near future, I will add code to support code that uses pthreads but only requires one thread. (i.e., to support almost every thread-safe library)
Tests involving the standard Regex crate

alastairreid · 2021-02-09T11:39:07Z

Note that this change should not be pushed for review until the script_fixes_2 change is merged.

verification-annotations/src/klee.rs

runtime/Makefile

fshaked · 2021-02-15T10:10:24Z

verification-annotations/src/tests.rs

+        verifier::assume(i.is_ascii_alphabetic());
+    }
+
+    for i in a.as_bytes().iter() {


Do you need the .iter() here? for does that for you. You can also do all this in one assertion:

verifier::assert!(a.as_bytes().iter().all(char::is_ascii))

I'm dropping the .iter() here and in the other place that I used '.as_bytes().iter()' a few lines above.

But I find that this point-free style less readable so I prefer the for loop.

fshaked · 2021-02-19T15:17:40Z

verification-annotations/src/klee.rs

+    }
+    match String::from_utf8(r) {
+        Ok(r) => r,
+        Err(_) => reject(),


Maybe this doesn't matter very much, but shouldn't this reject() be unreachable()?

reject() is equivalent to assume(false) and so it prevents the verifier from reporting errors involving this path. (In KLEE, it silently halts the current path exploration.)

unreachable() generates an error that is treated as a verification error.

In this case, the function is meant to be generating a legal string so we would not want to report an error.

But you already assume all the bytes are ascii, is the Err branch still reachable?

Ah, I see.

I am 99.9999% certain that this cannot fail.
But suppose I am wrong, then I would not want to report 'unreachable' because it would be an error in the verification support code not in the code being verified.

It would be good though to get some sort of report that there is a problem in the verification harness.
We should think about this a bit.

I think that this relates to a general problem in verification where you accidentally over-constrain the inputs so that you are not testing inputs that actually matter. In the extreme case (that is surprisingly common), the constraints are contradictory so there are no inputs and the verification is vacuously true.
I have been thinking that we should tackle that using a variation of what hardware engineers do when doing random testing: the System Verilog language lets you gather statistics about how many of the random inputs are in certain ranges - if a given range doesn't have enough values in it, you either need to test more or modify your test.
This would make sense as a proptest extension while for propverify we would just check that each range of interest is satisfiable.
(But exploring this is a problem for the future)

fshaked · 2021-02-19T15:27:12Z

verification-annotations/src/tests.rs

+#[cfg_attr(feature = "verifier-crux", crux_test)]
+fn bytes() {
+    let a = verifier::verifier_nondet_bytes(8);
+    for i in a.iter() {


for i in &a { will call a.iter(). Note the &, otherwise it calls a.into_iter() which moves a and you can no longer use it.

fshaked · 2021-02-19T15:28:46Z

verification-annotations/src/tests.rs

+    }
+
+    // force string to be a legal int
+    for i in a.as_bytes().into_iter() {


Don't need .into_iter().

fshaked · 2021-02-19T15:30:28Z

verification-annotations/src/tests.rs

+    }
+
+    // force string to be a legal int
+    for i in a.as_bytes().into_iter() {


Don't need .into_iter().

alastairreid · 2021-02-23T18:36:46Z

Sorry this is taking a while to get back to - I wanted to get KLEE up and running with the new cargo-verify frontend before revisiting this.
It will probably be a few days before I get back to this.

This is primarily a test that stubbing out feature tests and implementing posix_memalign fixes the problems we were seeing when trying to use the Regex library. As expected, the Regex library is a major verification bottleneck and you can only use very small, simple regexes. So regexes are still not viable to use at the moment.

alastairreid · 2021-03-11T11:31:20Z

I acted on all comments apart from the one about using unreachable instead of reject.
(Neither is perfect (see discussion above) - but I think that reject is closer.)

Also, I moved the regex tests into demos/bottlenecks/regex since they were more about testing our ability to cope with language/tool features than they were about testing the verification annotations crate.

(Since I have fixed everything, I would normally self-approve. But that seems to be disabled.)

alastairreid · 2021-03-11T11:32:09Z

(It wasn't disabled after all - confusing UI)

google-cla bot added the cla: yes Contributor has signed CLA label Feb 9, 2021

fshaked reviewed Feb 15, 2021

View reviewed changes

alastairreid force-pushed the strings branch from 02eea57 to 1749b17 Compare February 15, 2021 11:35

alastairreid marked this pull request as ready for review February 16, 2021 13:25

fshaked suggested changes Feb 19, 2021

View reviewed changes

Alastair Reid added 3 commits March 10, 2021 14:52

Annotations/KLEE: allocate symbolic Vec<u8>

166b2f7

Annotations/KLEE: Tests for Vec<u8> and strings

03a7b13

alastairreid force-pushed the strings branch from 007a13f to 56a506e Compare March 11, 2021 11:26

alastairreid merged commit a209a86 into project-oak:main Mar 11, 2021

alastairreid deleted the strings branch March 11, 2021 11:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for symbolic strings #88

Support for symbolic strings #88

alastairreid commented Feb 9, 2021 •

edited

alastairreid commented Feb 9, 2021

fshaked Feb 15, 2021

alastairreid Feb 15, 2021

fshaked Feb 19, 2021

alastairreid Feb 19, 2021

fshaked Feb 19, 2021

alastairreid Feb 19, 2021

fshaked Feb 19, 2021

fshaked Feb 19, 2021

fshaked Feb 19, 2021

alastairreid commented Feb 23, 2021

alastairreid commented Mar 11, 2021

alastairreid commented Mar 11, 2021

Support for symbolic strings #88

Support for symbolic strings #88

Conversation

alastairreid commented Feb 9, 2021 • edited

alastairreid commented Feb 9, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alastairreid commented Feb 23, 2021

alastairreid commented Mar 11, 2021

alastairreid commented Mar 11, 2021

alastairreid commented Feb 9, 2021 •

edited