Add some experimental support for non-lexical flow-typing rules

Add a file nl_flow.ml which can analyse a block of Sail expressions
and insert constraints for flow-typing rules which do not follow the
lexical structure of the code (and therefore the syntax-directed
typing rules can't do any flow-typing for). A common case found in ASL
translated Sail would be something like

function decode(Rt: bits(4)) = {
  if Rt == 0xF then {
    throw(Error_see("instruction"));
  };
  let t = unsigned(Rt);
  execute(t)
}

which would currently fail is execute has a 0 <= t <= 14 constraint
for a register it writes to. However if we spot this pattern and add
an assertion automatically:

  let t = unsigned(Rt);
  assert(t != 15);
  execute(t)

Then everything works, because the assertion is in the correct place
for regular flow typing. Currently it only works for this specific
use-case, and is turned on using the -non_lexical_flow flag

1 files changed, 118 insertions, 0 deletions

diff --git a/src/nl_flow.ml b/src/nl_flow.ml
new file mode 100644
index 00000000..e38e5fa5
--- /dev/null
+++ b/src/nl_flow.ml
@@ -0,0 +1,118 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+
+let opt_nl_flow = ref false
+
+let rec escapes (E_aux (aux, _)) =
+  match aux with
+  | E_throw _ -> true
+  | E_block [] -> false
+  | E_block exps -> escapes (List.hd (List.rev exps))
+  | _ -> false
+
+let is_bitvector_literal (L_aux (aux, _)) =
+  match aux with
+  | L_bin _ | L_hex _ -> true
+  | _ -> false
+
+let bitvector_unsigned (L_aux (aux, _)) =
+  let open Sail_lib in
+  match aux with
+  | L_bin str -> uint (List.map bin_char (Util.string_to_list str))
+  | L_hex str -> uint (bits_of_string str)
+  | _ -> assert false
+
+let rec pat_id (P_aux (aux, _)) =
+  match aux with
+  | P_id id -> Some id
+  | P_as (_, id) -> Some id
+  | P_var (pat, _) -> pat_id pat
+  | _ -> None
+
+let add_assert cond (E_aux (aux, (l, ())) as exp) =
+  let msg = mk_lit_exp (L_string "") in
+  let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (cond, msg))) in
+  match aux with
+  | E_block exps -> E_aux (E_block (assertion :: exps), (l, ()))
+  | _ -> E_aux (E_block (assertion :: [exp]), (l, ()))
+
+(* If we know that x != bitv, then after any let y = unsigned(x) we
+   will also know that y != unsigned(bitv) *)
+let modify_unsigned id value (E_aux (aux, annot) as exp) =
+  match aux with
+  | E_let (LB_aux (LB_val (pat, E_aux (E_app (f, [E_aux (E_id id', _)]), _)), _) as lb, exp')
+       when string_of_id f = "unsigned" && Id.compare id id' = 0 ->
+     begin match pat_id pat with
+     | None -> exp
+     | Some uid ->
+        E_aux (E_let (lb,
+                      add_assert (mk_exp (E_app_infix (mk_exp (E_id uid), mk_id "!=", mk_lit_exp (L_num value)))) exp'),
+               annot)
+     end
+  | _ -> exp
+
+let analyze' exps =
+  match exps with
+  | E_aux (E_if (cond, then_exp, _), _) :: rest when escapes then_exp ->
+     begin match cond with
+     | E_aux (E_app_infix (E_aux (E_id id, _), op, E_aux (E_lit lit, _)), _)
+     | E_aux (E_app_infix (E_aux (E_lit lit, _), op, E_aux (E_id id, _)), _)
+          when string_of_id op = "==" && is_bitvector_literal lit ->
+        let value = bitvector_unsigned lit in
+        List.map (modify_unsigned id value) exps
+     | _ -> exps
+     end
+  | _ -> exps
+
+let analyze exps =
+  if !opt_nl_flow then analyze' exps else exps