diff options
| author | Alasdair Armstrong | 2019-05-09 18:39:48 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-09 18:53:53 +0100 |
| commit | 7280e7bcdcb56521482846af3282f6adbd277ce0 (patch) | |
| tree | 9a6122b8979f6c29e1c7b035b7b20e76570e7c68 /lib/string.sail | |
| parent | 31d01d0997f94e57f251087ac4e0d084f538fffb (diff) | |
SMT: Make path conditionals more precise
Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.
This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.
I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.
Diffstat (limited to 'lib/string.sail')
| -rw-r--r-- | lib/string.sail | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/string.sail b/lib/string.sail index 3fe74eb5..87e4da57 100644 --- a/lib/string.sail +++ b/lib/string.sail @@ -5,6 +5,8 @@ $include <arith.sail> val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool +overload operator == = {eq_string} + infixl 9 ^-^ val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string |