diff options
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 2 | ||||
| -rw-r--r-- | src/rewriter.ml | 6 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 |
4 files changed, 8 insertions, 4 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index a9201c1f..d652d490 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -970,6 +970,8 @@ let generate_undefineds vs_ids (Defs defs) = gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; (* FIXME: How to handle inc/dec order correctly? *) gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; + (* Only used with lem_mwords *) + gen_vs (mk_id "undefined_bitvector") "forall 'n 'm. (atom('n), atom('m)) -> vector('n, 'm, dec,bit) effect {undef}"; gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] in let undefined_tu = function diff --git a/src/process_file.ml b/src/process_file.ml index 18df5047..59518075 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -259,6 +259,6 @@ let rewrite rewriters defs = exit 1 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] -let rewrite_undefined = rewrite [("undefined", Rewriter.rewrite_undefined)] +let rewrite_undefined = rewrite [("undefined", fun x -> Rewriter.rewrite_undefined !opt_lem_mwords x)] let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml diff --git a/src/rewriter.ml b/src/rewriter.ml index 60beadac..69beac4d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2512,11 +2512,13 @@ let rewrite_overload_cast (Defs defs) = let defs = List.map simple_def defs in Defs (List.filter (fun def -> not (is_overload def)) defs) -let rewrite_undefined = - let rec undefined_of_typ (Typ_aux (typ_aux, _)) = +let rewrite_undefined mwords = + let rec undefined_of_typ (Typ_aux (typ_aux, _) as typ) = match typ_aux with | Typ_id id -> mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit])) + | Typ_app (_,[start;size;_;_]) when mwords && is_bitvector_typ typ -> + mk_exp (E_app (mk_id "undefined_bitvector", undefined_of_typ_args start @ undefined_of_typ_args size)) | Typ_app (id, args) -> mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args))) | Typ_var kid -> diff --git a/src/rewriter.mli b/src/rewriter.mli index 73337de4..3125c410 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -56,7 +56,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs -val rewrite_undefined : tannot defs -> tannot defs +val rewrite_undefined : bool -> tannot defs -> tannot defs val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*) val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*) |