summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/nl_flow.ml118
-rw-r--r--src/nl_flow.mli60
-rw-r--r--src/sail.ml3
-rw-r--r--src/type_check.ml2
4 files changed, 182 insertions, 1 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
diff --git a/src/nl_flow.mli b/src/nl_flow.mli
new file mode 100644
index 00000000..f2bf0035
--- /dev/null
+++ b/src/nl_flow.mli
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(* 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
+
+(** [opt_nl_flow] must be true for [analyze] to do anything. *)
+val opt_nl_flow : bool ref
+
+(** Analyze a basic block for flow typing properties that do not
+ follow the lexical structure of the code (and therefore the
+ syntax-directed typing rules), and insert assertions for discovered
+ constraints *)
+val analyze : unit exp list -> unit exp list
diff --git a/src/sail.ml b/src/sail.ml
index 0d26df9c..59190d15 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -194,6 +194,9 @@ let options = Arg.align ([
( "-enum_casts",
Arg.Set Initial_check.opt_enum_casts,
" allow enumerations to be automatically casted to numeric range types");
+ ( "-non_lexical_flow",
+ Arg.Set Nl_flow.opt_nl_flow,
+ " allow non-lexical flow typing");
( "-no_lexp_bounds_check",
Arg.Set Type_check.opt_no_lexp_bounds_check,
" turn off bounds checking for vector assignments in l-expressions");
diff --git a/src/type_check.ml b/src/type_check.ml
index df074567..8b6a9c45 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2156,7 +2156,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let rec check_block l env exps typ =
let annot_exp_effect exp typ eff exp_typ = E_aux (exp, (l, Some ((env, typ, eff), exp_typ))) in
let annot_exp exp typ exp_typ = annot_exp_effect exp typ no_effect exp_typ in
- match exps with
+ match Nl_flow.analyze exps with
| [] -> typ_equality l env typ unit_typ; []
| [exp] -> [crule check_exp env exp typ]
| (E_aux (E_assign (lexp, bind), _) :: exps) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:55:05 +0000