From feb3d6f6e3ac8eec7fe700b55d590dbfbad891b3 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 29 Feb 2024 13:54:55 +0000 Subject: [PATCH] Improve interpreter value printing Some interpreter values printed in a slightly odd way, particularly enums which were treated like constructors and therefore got printed as `X()` for an enumeration member `X` which is not valid syntax. This means that SMT counterexamples should be pasteable into the interpreter more easily now --- src/lib/constant_fold.ml | 4 ++-- src/lib/interpreter.ml | 4 ++-- src/lib/value.ml | 11 +++++++++-- src/sail_smt_backend/smtlib.ml | 2 +- 4 files changed, 14 insertions(+), 7 deletions(-) diff --git a/src/lib/constant_fold.ml b/src/lib/constant_fold.ml index 9eadae09b..7c25d0e15 100644 --- a/src/lib/constant_fold.ml +++ b/src/lib/constant_fold.ml @@ -90,7 +90,7 @@ and exp_of_value = | V_bool true -> mk_lit_exp L_true | V_bool false -> mk_lit_exp L_false | V_string str -> mk_lit_exp (L_string str) - | V_record ctors -> mk_exp (E_struct (List.map fexp_of_ctor (StringMap.bindings ctors))) + | V_record fields -> mk_exp (E_struct (List.map fexp_of_ctor (StringMap.bindings fields))) | V_vector vs -> mk_exp (E_vector (List.map exp_of_value vs)) | V_tuple vs -> mk_exp (E_tuple (List.map exp_of_value vs)) | V_unit -> mk_lit_exp L_unit @@ -103,7 +103,7 @@ and exp_of_value = let rec is_too_large = let open Value in function - | V_int _ | V_bit _ | V_bool _ | V_string _ | V_unit | V_attempted_read _ | V_real _ | V_ref _ -> false + | V_int _ | V_bit _ | V_bool _ | V_string _ | V_unit | V_attempted_read _ | V_real _ | V_ref _ | V_member _ -> false | V_vector vs | V_tuple vs | V_list vs -> List.compare_length_with vs 256 > 0 | V_record fields -> StringMap.exists (fun _ v -> is_too_large v) fields | V_ctor (_, vs) -> List.exists is_too_large vs diff --git a/src/lib/interpreter.ml b/src/lib/interpreter.ml index e268a8231..e859ee940 100644 --- a/src/lib/interpreter.ml +++ b/src/lib/interpreter.ml @@ -468,7 +468,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = get_global_letbinds () >>= fun lbs -> let chain = build_letchain id lbs orig_exp in return chain - | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, []))) + | Enum _ -> return (exp_of_value (V_member (string_of_id id))) | _ -> fail ("Couldn't find id " ^ string_of_id id) end | E_struct fexps -> @@ -651,7 +651,7 @@ and pattern_match env (P_aux (p_aux, (l, _))) value = begin match Env.lookup_id id env with | Enum _ -> - if is_ctor value && string_of_id id = fst (coerce_ctor value) then (true, Bindings.empty) + if is_member value && string_of_id id = coerce_member value then (true, Bindings.empty) else (false, Bindings.empty) | _ -> (true, Bindings.singleton id (Complete_binding value)) end diff --git a/src/lib/value.ml b/src/lib/value.ml index c346c4d35..61b52b27e 100644 --- a/src/lib/value.ml +++ b/src/lib/value.ml @@ -97,6 +97,7 @@ type value = | V_unit | V_string of string | V_ref of string + | V_member of string | V_ctor of string * value list | V_record of value StringMap.t (* When constant folding we disable reading registers, so a register @@ -124,10 +125,11 @@ let rec string_of_value = function | V_string str -> "\"" ^ str ^ "\"" | V_ref str -> "ref " ^ str | V_real r -> Sail_lib.string_of_real r + | V_member str -> 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) + "struct {" + ^ Util.string_of_list ", " (fun (field, v) -> field ^ " = " ^ string_of_value v) (StringMap.bindings record) ^ "}" | V_attempted_read _ -> assert false @@ -143,11 +145,14 @@ let rec eq_value v1 v2 = | V_unit, V_unit -> true | V_string str1, V_string str2 -> str1 = str2 | V_ref str1, V_ref str2 -> str1 = str2 + | V_member name1, V_member name2 -> name1 = name2 | V_ctor (name1, fields1), V_ctor (name2, fields2) when List.length fields1 = List.length fields2 -> name1 = name2 && List.for_all2 eq_value fields1 fields2 | V_record fields1, V_record fields2 -> StringMap.equal eq_value fields1 fields2 | _, _ -> false +let coerce_member = function V_member str -> str | _ -> assert false + let coerce_ctor = function V_ctor (str, vals) -> (str, vals) | _ -> assert false let coerce_bool = function V_bool b -> b | _ -> assert false @@ -399,6 +404,8 @@ let value_count_leading_zeros = function | [v1] -> V_int (Sail_lib.count_leading_zeros (coerce_bv v1)) | _ -> failwith "value count_leading_zeros" +let is_member = function V_member _ -> true | _ -> false + let is_ctor = function V_ctor _ -> true | _ -> false let value_sign_extend = function diff --git a/src/sail_smt_backend/smtlib.ml b/src/sail_smt_backend/smtlib.ml index aebd360e0..393d43e3c 100644 --- a/src/sail_smt_backend/smtlib.ml +++ b/src/sail_smt_backend/smtlib.ml @@ -655,7 +655,7 @@ let rec value_of_sexpr sexpr = match sexpr with | Atom name -> begin match List.find_opt (fun member -> Util.zencode_string (string_of_id member) = name) members with - | Some member -> V_ctor (string_of_id member, []) + | Some member -> V_member (string_of_id member) | None -> failwith ("Could not find enum member for " ^ name ^ " in " ^ Util.string_of_list ", " string_of_id members)