From 7280e7bcdcb56521482846af3282f6adbd277ce0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 9 May 2019 18:39:48 +0100
Subject: 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.
---
 lib/mapping.sail | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 lib/real.sail    |  4 +--
 lib/string.sail  |  2 ++
 3 files changed, 88 insertions(+), 2 deletions(-)
 create mode 100644 lib/mapping.sail

(limited to 'lib')

diff --git a/lib/mapping.sail b/lib/mapping.sail
new file mode 100644
index 00000000..6cbb7585
--- /dev/null
+++ b/lib/mapping.sail
@@ -0,0 +1,84 @@
+$ifndef _MAPPING
+$define _MAPPING
+
+$include <arith.sail>
+$include <option.sail>
+
+val string_take = "string_take" : (string, nat) -> string
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+val string_startswith = "string_startswith" : (string, string) -> bool
+
+val n_leading_spaces : string -> nat
+function n_leading_spaces s =
+  match s {
+    "" => 0,
+    _ => match string_take(s, 1) {
+      " " => 1 + n_leading_spaces(string_drop(s, 1)),
+      _ => 0
+    }
+  }
+
+val spc     : unit <-> string
+val opt_spc : unit <-> string
+val def_spc : unit <-> string
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+val spc_matches_prefix : string -> option((unit, nat))
+function spc_matches_prefix s = {
+  let n = n_leading_spaces(s);
+  match n {
+    0 => None(),
+    _ => Some((), n)
+  }
+}
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+val opt_spc_matches_prefix : string -> option((unit, nat))
+function opt_spc_matches_prefix s =
+  Some((), n_leading_spaces(s))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+val def_spc_matches_prefix : string -> option((unit, nat))
+function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
+
+val sep : unit <-> string
+mapping sep : unit <-> string = {
+  ()     <-> opt_spc() ^ "," ^ def_spc()
+}
+
+$ifdef _DEFAULT_DEC
+$include <vector_dec.sail>
+
+val hex_bits_20 : bits(20) <-> string
+val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
+val hex_bits_20_forwards_matches : bits(20) -> bool
+function hex_bits_20_forwards_matches bv = true
+val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+val hex_bits_20_backwards_matches : string -> bool
+function hex_bits_20_backwards_matches s = match s {
+  s if match hex_bits_20_matches_prefix(s) {
+    Some (_, n) if n == string_length(s) => true,
+    _ => false
+  } => true,
+  _ => false
+}
+val hex_bits_20_backwards : string -> bits(20)
+function hex_bits_20_backwards s =
+  match hex_bits_20_matches_prefix(s) {
+      Some (bv, n) if n == string_length(s) => bv
+  }
+
+$endif
+
+$endif
diff --git a/lib/real.sail b/lib/real.sail
index 47d3f9bd..cd63a622 100644
--- a/lib/real.sail
+++ b/lib/real.sail
@@ -1,5 +1,5 @@
-$ifndef __REAL
-$define __REAL
+$ifndef _REAL
+$define _REAL
 
 val "neg_real" : real -> real
 
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
-- 
cgit v1.2.3