summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--editors/sail2-mode.el9
-rw-r--r--language/l2.ott2
-rw-r--r--src/ast_util.ml2
-rw-r--r--src/initial_check.ml1
-rw-r--r--src/interpreter.ml67
-rw-r--r--src/isail.ml2
-rw-r--r--src/lexer2.mll8
-rw-r--r--src/parse_ast.ml1
-rw-r--r--src/parser2.mly2
-rw-r--r--src/pretty_print_sail2.ml2
-rw-r--r--src/process_file.ml1
-rw-r--r--src/process_file.mli1
-rw-r--r--src/rewriter.ml11
-rw-r--r--src/rewriter.mli2
-rw-r--r--src/rewrites.ml8
-rw-r--r--src/rewrites.mli3
-rw-r--r--src/sail.ml2
-rw-r--r--src/type_check.ml19
-rw-r--r--src/value.ml15
19 files changed, 127 insertions, 31 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 7a420f14..26301d0f 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -34,13 +34,8 @@
(modify-syntax-entry ?_ "w" st)
(modify-syntax-entry ?' "w" st)
(modify-syntax-entry ?* ". 23" st)
- (condition-case nil
- (progn
- (modify-syntax-entry ?\( "()1n" st)
- (modify-syntax-entry ?\) ")(4n" st))
- (error ; XEmacs signals an error instead of ignoring `n'.
- (modify-syntax-entry ?\( "()1" st)
- (modify-syntax-entry ?\) ")(4" st)))
+ (modify-syntax-entry ?/ ". 124b" st)
+ (modify-syntax-entry ?\n "> b" st)
st)
"Syntax table for Sail2 mode")
diff --git a/language/l2.ott b/language/l2.ott
index ea4a8a6a..d26073f5 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -826,6 +826,8 @@ exp :: 'E_' ::=
lexp :: 'LEXP_' ::= {{ com lvalue expression }}
{{ aux _ annot }} {{ auxparam 'a }}
| id :: :: id
+% | ref id :: :: ref
+ | deref exp :: :: deref
{{ com identifier }}
| id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }}
| id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 4407b7f1..7e966bf2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -413,6 +413,7 @@ and map_letbind_annot_aux f = function
and map_lexp_annot f (LEXP_aux (lexp, annot)) = LEXP_aux (map_lexp_annot_aux f lexp, f annot)
and map_lexp_annot_aux f = function
| LEXP_id id -> LEXP_id id
+ | LEXP_deref exp -> LEXP_deref (map_exp_annot f exp)
| LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps)
| LEXP_cast (typ, id) -> LEXP_cast (typ, id)
| LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps)
@@ -660,6 +661,7 @@ and string_of_pat (P_aux (pat, l)) =
and string_of_lexp (LEXP_aux (lexp, _)) =
match lexp with
| LEXP_id v -> string_of_id v
+ | LEXP_deref exp -> "*(" ^ string_of_exp exp ^ ")"
| LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v
| LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")"
| LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 0915bc38..d7b69c4f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -528,6 +528,7 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l
LEXP_aux(
(match exp with
| Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
+ | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp)
| Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id)
| Parse_ast.E_tuple(tups) ->
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 4fd75094..7e84f5c7 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -53,20 +53,30 @@ open Ast_util
open Value
type gstate =
- { registers : value Bindings.t }
+ { registers : value Bindings.t;
+ letbinds : (Type_check.tannot letbind) list
+ }
type lstate =
{ locals : value Bindings.t }
type state = lstate * gstate
-let initial_gstate =
- { registers = Bindings.empty }
+let rec ast_letbinds (Defs defs) =
+ match defs with
+ | [] -> []
+ | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
+ | _ :: defs -> ast_letbinds (Defs defs)
+
+let initial_gstate ast =
+ { registers = Bindings.empty;
+ letbinds = ast_letbinds ast
+ }
let initial_lstate =
{ locals = Bindings.empty }
-let initial_state = initial_lstate, initial_gstate
+let initial_state ast = initial_lstate, initial_gstate ast
let value_of_lit (L_aux (l_aux, _)) =
match l_aux with
@@ -77,6 +87,11 @@ let value_of_lit (L_aux (l_aux, _)) =
| L_false -> V_bool false
| L_string str -> V_string str
| L_num n -> V_int n
+ | L_hex str ->
+ Util.string_to_list str
+ |> List.map (fun c -> List.map (fun b -> V_bit b) (Sail_lib.hex_char c))
+ |> List.concat
+ |> (fun v -> V_vector v)
| _ -> failwith "Unimplemented value_of_lit" (* TODO *)
let is_value = function
@@ -175,7 +190,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
| E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps)
| E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2)
| E_tuple exps -> E_tuple (List.map (subst id value) exps)
- | E_assign (lexp, exp) -> E_assign (lexp, subst id value exp) (* Shadowing... *)
+ | E_assign (lexp, exp) -> E_assign (subst_lexp id value lexp, subst id value exp) (* Shadowing... *)
| E_let (LB_aux (LB_val (pat, bind), lb_annot), body) ->
(* TODO: Fix shadowing *)
E_let (LB_aux (LB_val (pat, subst id value bind), lb_annot), subst id value body)
@@ -189,6 +204,16 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
in
wrap e_aux
+and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) =
+ let wrap lexp_aux = LEXP_aux (lexp_aux, annot) in
+ let lexp_aux = match lexp_aux with
+ | LEXP_deref exp -> LEXP_deref (subst id value exp)
+ | LEXP_id id' -> LEXP_id id'
+ | LEXP_memory (f, exps) -> LEXP_memory (f, List.map (subst id value) exps)
+ | _ -> failwith ("subst lexp")
+ in
+ wrap lexp_aux
+
(**************************************************************************)
(* 2. Expression Evaluation *)
@@ -199,6 +224,14 @@ let unit_exp = E_lit (L_aux (L_unit, Parse_ast.Unknown))
let is_value_fexp (FE_aux (FE_Fexp (id, exp), _)) = is_value exp
let value_of_fexp (FE_aux (FE_Fexp (id, exp), _)) = (string_of_id id, value_of_exp exp)
+let rec build_letchain lbs (E_aux (_, annot) as exp) =
+ print_endline ("LETCHAIN " ^ string_of_exp exp);
+ match lbs with
+ | [] -> exp
+ | lb :: lbs ->
+ let exp = E_aux (E_let (lb, exp), annot) in
+ build_letchain lbs exp
+
let rec step (E_aux (e_aux, annot) as orig_exp) =
let wrap e_aux' = return (E_aux (e_aux', annot)) in
match e_aux with
@@ -246,6 +279,9 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
else
failwith "Match failure"
+ | E_vector_update (vec, n, x) ->
+ wrap (E_app (mk_id "vector_update", [vec; n; x]))
+
(* otherwise left-to-right evaluation order for function applications *)
| E_app (id, exps) ->
let evaluated, unevaluated = Util.take_drop is_value exps in
@@ -298,6 +334,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| E_throw exp when is_value exp -> throw (value_of_exp exp)
| E_throw exp -> step exp >>= fun exp' -> wrap (E_throw exp')
+ | E_ref id -> return (exp_of_value (V_ref (string_of_id id)))
| E_id id ->
begin
let open Type_check in
@@ -312,6 +349,10 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
in
return exp
| Local (Mutable, _) -> return (exp_of_value (Bindings.find id lstate.locals))
+ | Local (Immutable, _) ->
+ let chain = build_letchain gstate.letbinds orig_exp in
+ print_endline "CHAINED";
+ return chain
| _ -> failwith "id"
end
@@ -355,6 +396,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
let ul = (Parse_ast.Unknown, None) in
let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in
wrap (E_assign (lexp, exp'))
+ | E_assign (LEXP_aux (LEXP_vector (vec, n), _), exp) ->
+ let open Type_check in
+ let vec_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp vec)) in
+ let ul = (Parse_ast.Unknown, None) in
+ let exp' = E_aux (E_vector_update (vec_exp, n, exp), ul) in
+ wrap (E_assign (vec, exp'))
| E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) ->
begin
let open Type_check in
@@ -366,6 +413,12 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
puts ({ lstate with locals = Bindings.add id (value_of_exp exp) lstate.locals }, gstate) >> wrap unit_exp
| _ -> failwith "Assign"
end
+ | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) when not (is_value reference) ->
+ step reference >>= fun reference' -> wrap (E_assign (LEXP_aux (LEXP_deref reference', annot), exp))
+ | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) ->
+ let id = Id_aux (Id (coerce_ref (value_of_exp reference)), Parse_ast.Unknown) in
+ gets >>= fun (lstate, gstate) ->
+ puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp
| E_assign _ -> assert false
| E_try (exp, pexps) when is_value exp -> return exp
@@ -443,7 +496,7 @@ let rec get_fundef id (Defs defs) =
let stack_cont (_, _, cont) = cont
let stack_string (str, _, _) = str
let stack_state (_, lstate, _) = lstate
-
+
type frame =
| Done of state * value
| Step of string * state * (Type_check.tannot exp) monad * (string * lstate * (value -> (Type_check.tannot exp) monad)) list
@@ -473,5 +526,5 @@ let rec eval_frame ast = function
print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear);
Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
| Yield (Assertion_failed msg), _ ->
- failwith msg
+ failwith msg
| _ -> assert false
diff --git a/src/isail.ml b/src/isail.ml
index 88835b8a..3df9c8f1 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -127,7 +127,7 @@ let handle_input input =
| _ -> print_endline ("Unrecognised command " ^ input)
else if input <> "" then
let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord input) in
- current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state, return exp, [])))
+ current_mode := Evaluation (eval_frame !interactive_ast (Step ("", initial_state !interactive_ast, return exp, [])))
else ()
end
| Evaluation frame ->
diff --git a/src/lexer2.mll b/src/lexer2.mll
index b293046f..312183fa 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -231,6 +231,8 @@ rule token = parse
| "->" { MinusGt }
| "=>" { EqGt(r "=>") }
| "<=" { (LtEq(r"<=")) }
+ | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
+ | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
| "infix" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
@@ -243,8 +245,6 @@ rule token = parse
| operator as op
{ try M.find op !operators
with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
- | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
- | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
| tyvar_start startident ident* as i { TyVar(r i) }
| "~" { Id(r"~") }
| startident ident* as i { if M.mem i kw_table then
@@ -269,8 +269,8 @@ rule token = parse
and comment pos depth = parse
- | "(*" { comment pos (depth+1) lexbuf }
- | "*)" { if depth = 0 then ()
+ | "/*" { comment pos (depth+1) lexbuf }
+ | "*/" { if depth = 0 then ()
else if depth > 0 then comment pos (depth-1) lexbuf
else assert false }
| "\n" { Lexing.new_line lexbuf;
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 83b116a2..e84e8a60 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -268,6 +268,7 @@ exp_aux = (* Expression *)
| E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
| E_id of id (* identifier *)
| E_ref of id
+ | E_deref of exp
| E_lit of lit (* literal constant *)
| E_cast of atyp * exp (* cast *)
| E_app of id * (exp) list (* function application *)
diff --git a/src/parser2.mly b/src/parser2.mly
index ebe829c2..34ab8732 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -714,6 +714,8 @@ exp:
{ mk_exp (E_let ($2, $4)) $startpos $endpos }
| Var atomic_exp Eq exp In exp
{ mk_exp (E_var ($2, $4, $6)) $startpos $endpos }
+ | Star atomic_exp
+ { mk_exp (E_deref $2) $startpos $endpos }
| Lcurly block Rcurly
{ mk_exp (E_block $2) $startpos $endpos }
| Return exp
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 22b6e9ee..930da39c 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -357,6 +357,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
separate space [doc_atomic_exp exp; colon; doc_typ typ]
| E_lit lit -> doc_lit lit
| E_id id -> doc_id id
+ | E_ref id -> string "ref" ^^ space ^^ doc_id id
| E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id
| E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid
| E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp)
@@ -395,6 +396,7 @@ and doc_lexp (LEXP_aux (l_aux, _) as lexp) =
and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
match l_aux with
| LEXP_id id -> doc_id id
+ | LEXP_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen
| LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen
| LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
| LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
diff --git a/src/process_file.ml b/src/process_file.ml
index d57127a4..8c00d37b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -236,5 +236,6 @@ let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)]
let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
+let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil
let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check
diff --git a/src/process_file.mli b/src/process_file.mli
index f99bdf54..86e8fb05 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -56,6 +56,7 @@ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_sil : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/rewriter.ml b/src/rewriter.ml
index fb82b80f..53a43e5b 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -107,7 +107,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
let effsum = match e with
| E_block es -> union_eff_exps es
| E_nondet es -> union_eff_exps es
- | E_id _
+ | E_id _ | E_ref _
| E_lit _ -> eff
| E_cast (_,e) -> effect_of e
| E_app (f,es) ->
@@ -339,6 +339,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
let rewrap le = LEXP_aux(le,(l,annot)) in
match lexp with
| LEXP_id _ | LEXP_cast _ -> rewrap lexp
+ | LEXP_deref exp -> rewrap (LEXP_deref (rewriters.rewrite_exp rewriters exp))
| LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters) tupls))
| LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters) exps))
| LEXP_vector (lexp,exp) ->
@@ -472,6 +473,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
{ e_block : 'exp list -> 'exp_aux
; e_nondet : 'exp list -> 'exp_aux
; e_id : id -> 'exp_aux
+ ; e_ref : id -> 'exp_aux
; e_lit : lit -> 'exp_aux
; e_cast : Ast.typ * 'exp -> 'exp_aux
; e_app : id * 'exp list -> 'exp_aux
@@ -512,6 +514,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; e_internal_value : Value.value -> 'exp_aux
; e_aux : 'exp_aux * 'a annot -> 'exp
; lEXP_id : id -> 'lexp_aux
+ ; lEXP_deref : 'exp -> 'lexp_aux
; lEXP_memory : id * 'exp list -> 'lexp_aux
; lEXP_cast : Ast.typ * id -> 'lexp_aux
; lEXP_tup : 'lexp list -> 'lexp_aux
@@ -538,6 +541,7 @@ let rec fold_exp_aux alg = function
| E_block es -> alg.e_block (List.map (fold_exp alg) es)
| E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es)
| E_id id -> alg.e_id id
+ | E_ref id -> alg.e_ref id
| E_lit lit -> alg.e_lit lit
| E_cast (typ,e) -> alg.e_cast (typ, fold_exp alg e)
| E_app (id,es) -> alg.e_app (id, List.map (fold_exp alg) es)
@@ -588,6 +592,7 @@ let rec fold_exp_aux alg = function
and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot)
and fold_lexp_aux alg = function
| LEXP_id id -> alg.lEXP_id id
+ | LEXP_deref exp -> alg.lEXP_deref (fold_exp alg exp)
| LEXP_memory (id,es) -> alg.lEXP_memory (id, List.map (fold_exp alg) es)
| LEXP_tup les -> alg.lEXP_tup (List.map (fold_lexp alg) les)
| LEXP_cast (typ,id) -> alg.lEXP_cast (typ,id)
@@ -618,6 +623,7 @@ let id_exp_alg =
{ e_block = (fun es -> E_block es)
; e_nondet = (fun es -> E_nondet es)
; e_id = (fun id -> E_id id)
+ ; e_ref = (fun id -> E_ref id)
; e_lit = (fun lit -> (E_lit lit))
; e_cast = (fun (typ,e) -> E_cast (typ,e))
; e_app = (fun (id,es) -> E_app (id,es))
@@ -658,6 +664,7 @@ let id_exp_alg =
; e_internal_value = (fun v -> E_internal_value v)
; e_aux = (fun (e,annot) -> E_aux (e,annot))
; lEXP_id = (fun id -> LEXP_id id)
+ ; lEXP_deref = (fun e -> LEXP_deref e)
; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es))
; lEXP_cast = (fun (typ,id) -> LEXP_cast (typ,id))
; lEXP_tup = (fun tups -> LEXP_tup tups)
@@ -712,6 +719,7 @@ let compute_exp_alg bot join =
{ e_block = split_join (fun es -> E_block es)
; e_nondet = split_join (fun es -> E_nondet es)
; e_id = (fun id -> (bot, E_id id))
+ ; e_ref = (fun id -> (bot, E_ref id))
; e_lit = (fun lit -> (bot, E_lit lit))
; e_cast = (fun (typ,(v,e)) -> (v, E_cast (typ,e)))
; e_app = (fun (id,es) -> split_join (fun es -> E_app (id,es)) es)
@@ -760,6 +768,7 @@ let compute_exp_alg bot join =
; e_internal_value = (fun v -> (bot, E_internal_value v))
; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot)))
; lEXP_id = (fun id -> (bot, LEXP_id id))
+ ; lEXP_deref = (fun (v, e) -> (v, LEXP_deref e))
; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es)
; lEXP_cast = (fun (typ,id) -> (bot, LEXP_cast (typ,id)))
; lEXP_tup = (fun ls ->
diff --git a/src/rewriter.mli b/src/rewriter.mli
index faa6a81a..c3c384bf 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -108,6 +108,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
{ e_block : 'exp list -> 'exp_aux
; e_nondet : 'exp list -> 'exp_aux
; e_id : id -> 'exp_aux
+ ; e_ref : id -> 'exp_aux
; e_lit : lit -> 'exp_aux
; e_cast : Ast.typ * 'exp -> 'exp_aux
; e_app : id * 'exp list -> 'exp_aux
@@ -148,6 +149,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; e_internal_value : Value.value -> 'exp_aux
; e_aux : 'exp_aux * 'a annot -> 'exp
; lEXP_id : id -> 'lexp_aux
+ ; lEXP_deref : 'exp -> 'lexp_aux
; lEXP_memory : id * 'exp list -> 'lexp_aux
; lEXP_cast : Ast.typ * id -> 'lexp_aux
; lEXP_tup : 'lexp list -> 'lexp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index a28352f5..87baa746 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -328,6 +328,7 @@ let rewrite_sizeof (Defs defs) =
{ e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es'))
; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es'))
; e_id = (fun id -> (E_id id, E_id id))
+ ; e_ref = (fun id -> (E_ref id, E_ref id))
; e_lit = (fun lit -> (E_lit lit, E_lit lit))
; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e')))
; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es')))
@@ -368,6 +369,7 @@ let rewrite_sizeof (Defs defs) =
; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
+ ; lEXP_deref = (fun (e, e') -> (LEXP_deref e, LEXP_deref e'))
; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id)))
; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
@@ -2955,6 +2957,12 @@ let rewrite_defs_ocaml = [
(* ("separate_numbs", rewrite_defs_separate_numbs) *)
]
+let rewrite_defs_interpreter = [
+ ("constraint", rewrite_constraint);
+ ("trivial_sizeof", rewrite_trivial_sizeof);
+ ("sizeof", rewrite_sizeof);
+ ]
+
let rewrite_defs_sil = [
("top_sort_defs", top_sort_defs);
("tuple_vector_assignments", rewrite_tuple_vector_assignments);
diff --git a/src/rewrites.mli b/src/rewrites.mli
index ce24a4c4..8fceadff 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -57,6 +57,9 @@ val rewrite_undefined : bool -> tannot defs -> tannot defs
(* Perform rewrites to exclude AST nodes not supported for ocaml out*)
val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list
+(* Perform rewrites to exclude AST nodes not supported for interpreter *)
+val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list
+
(* Perform rewrites to exclude AST nodes not supported for lem out*)
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list
diff --git a/src/sail.ml b/src/sail.ml
index 519ec916..d4e2526e 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -216,7 +216,7 @@ let main() =
begin
(if !(opt_interactive)
then
- (interactive_ast := ast; interactive_env := type_envs)
+ (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs)
else ());
(if !(opt_sanity)
then
diff --git a/src/type_check.ml b/src/type_check.ml
index 907c23a5..d3967e7d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2489,10 +2489,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
match lexp_aux with
+ | LEXP_deref exp ->
+ let inferred_exp = infer_exp env exp in
+ begin match typ_of inferred_exp with
+ | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "ref" ->
+ subtyp l env typ vtyp; annot_lexp (LEXP_deref inferred_exp) typ, env
+ | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
+ subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
+ end
| LEXP_id v ->
begin match Env.lookup_id v env with
- | Local (Immutable, Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _)) when string_of_id r = "ref" ->
- subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
| Local (Immutable, _) | Enum _ | Union _ ->
typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
@@ -2599,9 +2605,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| _ -> assert false
in
match typ_of access with
- | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
- subtyp l env typ deref_typ;
- annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
| _ when not is_immutable && is_register ->
subtyp l env typ (typ_of access);
annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
@@ -2627,9 +2630,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| _ -> assert false
in
match typ_of access with
- | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
- subtyp l env typ deref_typ;
- annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
| _ when not is_immutable && is_register ->
subtyp l env typ (typ_of access);
annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
@@ -3230,6 +3230,9 @@ and propagate_lexp_effect (LEXP_aux (lexp, annot)) =
add_effect_lexp (LEXP_aux (p_lexp, annot)) eff
and propagate_lexp_effect_aux = function
| LEXP_id id -> LEXP_id id, no_effect
+ | LEXP_deref exp ->
+ let p_exp = propagate_exp_effect exp in
+ LEXP_deref p_exp, effect_of p_exp
| LEXP_memory (id, exps) ->
let p_exps = List.map propagate_exp_effect exps in
LEXP_memory (id, p_exps), collect_effects p_exps
diff --git a/src/value.ml b/src/value.ml
index 59dadafe..d9690899 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -61,6 +61,7 @@ type value =
| V_tuple of value list
| V_unit
| V_string of string
+ | V_ref of string
| V_ctor of string * value list
| V_record of value StringMap.t
@@ -127,6 +128,10 @@ let coerce_string = function
| V_string str -> str
| _ -> assert false
+let coerce_ref = function
+ | V_ref str -> str
+ | _ -> assert false
+
let unit_value = V_unit
let value_eq_int = function
@@ -221,17 +226,23 @@ let value_replicate_bits = function
| [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2))
| _ -> failwith "value replicate_bits"
+let is_bit = function
+ | V_bit _ -> true
+ | _ -> false
+
let rec string_of_value = function
- | V_vector vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
+ | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
+ | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"
| V_bool true -> "true"
| V_bool false -> "false"
| V_bit B0 -> "bitzero"
| V_bit B1 -> "bitone"
| V_int n -> Big_int.to_string n
| V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
- | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
+ | V_list vals -> "[|" ^ Util.string_of_list ", " string_of_value vals ^ "|]"
| V_unit -> "()"
| V_string str -> "\"" ^ str ^ "\""
+ | V_ref str -> "ref " ^ str
| V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
| V_record record ->
"{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:19:53 +0000