[asl] Allow equality for string types.

herd · Apr 15, 2024 · e741986 · e741986
1 parent 19369a0
commit e741986
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/asllib/StaticInterpreter.ml b/asllib/StaticInterpreter.ml
@@ -124,6 +124,9 @@ let binop_values pos op v1 v2 =
       L_BitVector Bitvector.(of_z (length b1) (Z.add (to_z_unsigned b1) z2))
   | MINUS, L_BitVector b1, L_Int z2 ->
       L_BitVector Bitvector.(of_z (length b1) (Z.sub (to_z_unsigned b1) z2))
+  (* string -> string -> bool *)
+  | EQ_OP, L_String s1, L_String s2 -> L_Bool (String.equal s1 s2)
+  | NEQ, L_String s1, L_String s2 -> L_Bool (not (String.equal s1 s2))
   (* Failure *)
   | _ -> fatal_from pos (Error.UnsupportedBinop (op, v1, v2))
 

diff --git a/asllib/Typing.ml b/asllib/Typing.ml
@@ -658,14 +658,15 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
                      bitvectors then they must have the same determined
                      width. *)
                   check_bits_equal_width' env t1_anon t2_anon;
-                  (* The rest are redundancies from the first equal types
-                     cases, but provided for completeness. *)
                   both
                     (check_type_satisfies' env t1_anon boolean)
                     (check_type_satisfies' env t2_anon boolean);
                   both
                     (check_type_satisfies' env t1_anon real)
                     (check_type_satisfies' env t2_anon real);
+                  both
+                    (check_type_satisfies' env t1_anon string)
+                    (check_type_satisfies' env t2_anon string);
                   (fun () ->
                     match (t1_anon.desc, t2_anon.desc) with
                     | T_Enum li1, T_Enum li2 ->