start of string pattern matching: currently only literals

12 files changed, 171 insertions, 1 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2f2d27d8..0817e46c 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -438,6 +438,7 @@ and map_pat_annot_aux f = function
   | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
   | P_vector pats -> P_vector (List.map (map_pat_annot f) pats)
   | P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2)
+  | P_string_append (pat1, pat2) -> P_string_append (map_pat_annot f pat1, map_pat_annot f pat2)
 and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
 and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
 and map_letbind_annot_aux f = function
@@ -710,6 +711,7 @@ and string_of_pat (P_aux (pat, l)) =
   | P_vector_concat pats -> string_of_list " : " string_of_pat pats
   | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]"
   | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id
+  | P_string_append (pat1, pat2) -> string_of_pat pat1 ^ " ^^ " ^ string_of_pat pat2
   | _ -> "PAT"
 and string_of_lexp (LEXP_aux (lexp, _)) =
   match lexp with
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 62c1af02..a294d70a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -468,6 +468,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
     | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats)
     | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats)
     | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2)
+    | Parse_ast.P_string_append (pat1, pat2) -> P_string_append (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2)
     ), (l,()))
 
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 1fe2a849..f3d93d95 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -215,6 +215,7 @@ rule token = parse
   | "2" ws "^"                          { TwoCaret }
   | "^"					{ (Caret(r"^")) }
   | "::"                                { ColonColon(r "::") }
+  | "^^"                                { CaretCaret(r "^^") }
   | "~~"                                { TildeTilde(r "~~") }
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 635caa9c..f71498be 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -251,6 +251,7 @@ pat_aux =  (* Pattern *)
  | P_tup of (pat) list (* tuple pattern *)
  | P_list of (pat) list (* list pattern *)
  | P_cons of pat * pat (* cons pattern *)
+ | P_string_append of pat * pat (* string append pattern, x ^^ y *)
 
 and pat = 
    P_aux of pat_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index d126e253..cf2d50a7 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -177,7 +177,7 @@ let rec desugar_rchain chain s e =
 %token <string> String Bin Hex Real
 
 %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
-%token <string> Colon ColonColon TildeTilde ExclEq
+%token <string> Colon ColonColon CaretCaret TildeTilde ExclEq
 %token <string> GtEq
 %token <string> LtEq
 
@@ -651,6 +651,8 @@ pat1:
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
   | atomic_pat ColonColon pat1
     { mk_pat (P_cons ($1, $3)) $startpos $endpos }
+  | atomic_pat CaretCaret pat1
+    { mk_pat (P_string_append ($1, $3)) $startpos $endpos }
 
 pat_concat:
   | atomic_pat
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index c13452ff..3797354c 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -68,6 +68,7 @@ type gpat =
   | GP_cons of gpat * gpat
   | GP_app of (gpat Bindings.t)
   | GP_record of (gpat Bindings.t)
+  | GP_string_append of gpat * gpat
 
 let rec string_of_gpat = function
   | GP_lit lit -> string_of_lit lit
@@ -80,12 +81,14 @@ let rec string_of_gpat = function
   | GP_app app ->
      Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app)
   | GP_record _ -> "GP RECORD"
+  | GP_string_append (gpat1, gpat2) -> string_of_gpat gpat1 ^ " ^^" ^ string_of_gpat gpat2
 
 let is_wild = function
   | GP_wild -> true
   | _ -> false
 
 let rec generalize ctx (P_aux (p_aux, _) as pat) =
+
   match p_aux with
   | P_lit lit -> GP_lit lit
   | P_wild -> GP_wild
@@ -116,6 +119,10 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) =
      let ghd_pat = generalize ctx hd_pat in
      let gtl_pat = generalize ctx tl_pat in
      if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat)
+  | P_string_append (pat1, pat2) ->
+     let gpat1 = generalize ctx pat1 in
+     let gpat2 = generalize ctx pat2 in
+     if is_wild gpat1 && is_wild gpat2 then GP_wild else GP_string_append (gpat1, gpat2)
   | P_app (f, pats) ->
      let gpats = List.map (generalize ctx) pats in
      if List.for_all is_wild gpats then
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 203e8a58..63a1c77f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -304,6 +304,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
   | P_tup pats -> rewrap (P_tup (List.map rewrite pats))
   | P_list pats -> rewrap (P_list (List.map rewrite pats))
   | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2))
+  | P_string_append (pat1, pat2) -> rewrap (P_string_append (rewrite pat1, rewrite pat2))
 
 let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   let rewrap e = E_aux (e,(l,annot)) in
@@ -452,6 +453,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_tup            : 'pat list -> 'pat_aux
   ; p_list           : 'pat list -> 'pat_aux
   ; p_cons           : 'pat * 'pat -> 'pat_aux
+  ; p_string_append  : 'pat * 'pat -> 'pat_aux
   ; p_aux            : 'pat_aux * 'a annot -> 'pat
   ; fP_aux           : 'fpat_aux * 'a annot -> 'fpat
   ; fP_Fpat          : id * 'pat -> 'fpat_aux
@@ -472,6 +474,7 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
   | P_tup ps            -> alg.p_tup (List.map (fold_pat alg) ps)
   | P_list ps           -> alg.p_list (List.map (fold_pat alg) ps)
   | P_cons (ph,pt)      -> alg.p_cons (fold_pat alg ph, fold_pat alg pt)
+  | P_string_append (p1, p2) -> alg.p_string_append (fold_pat alg p1, fold_pat alg p2)
 
 and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat =
   function
@@ -498,6 +501,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   ; p_tup            = (fun ps -> P_tup ps)
   ; p_list           = (fun ps -> P_list ps)
   ; p_cons           = (fun (ph,pt) -> P_cons (ph,pt))
+  ; p_string_append  = (fun (p1,p2) -> P_string_append (p1,p2))
   ; p_aux            = (fun (pat,annot) -> P_aux (pat,annot))
   ; fP_aux           = (fun (fpat,annot) -> FP_aux (fpat,annot))
   ; fP_Fpat          = (fun (id,pat) -> FP_Fpat (id,pat))
@@ -744,6 +748,7 @@ let compute_pat_alg bot join =
   ; p_tup            = split_join (fun ps -> P_tup ps)
   ; p_list           = split_join (fun ps -> P_list ps)
   ; p_cons           = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt)))
+  ; p_string_append  = (fun ((v1,p1),(v2,p2)) -> (join v1 v2, P_string_append (p1,p2)))
   ; p_aux            = (fun ((v,pat),annot) -> (v, P_aux (pat,annot)))
   ; fP_aux           = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot)))
   ; fP_Fpat          = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat)))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index f8982d69..70c894c4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -95,6 +95,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_tup            : 'pat list -> 'pat_aux
   ; p_list           : 'pat list -> 'pat_aux
   ; p_cons           : 'pat * 'pat -> 'pat_aux
+  ; p_string_append  : 'pat * 'pat -> 'pat_aux
   ; p_aux            : 'pat_aux * 'a annot -> 'pat
   ; fP_aux           : 'fpat_aux * 'a annot -> 'fpat
   ; fP_Fpat          : id * 'pat -> 'fpat_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 591bc276..3b5a1736 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -676,6 +676,7 @@ let remove_vector_concat_pat pat =
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
     ; p_cons           = (fun (p,ps) -> P_cons (p false, ps false))
+    ; p_string_append  = (fun (p1,p2) -> P_string_append (p1 false, p2 false))
     ; p_aux =
         (fun (pat,((l,_) as annot)) contained_in_p_as ->
           match pat with
@@ -819,6 +820,7 @@ let remove_vector_concat_pat pat =
     ; p_list           = (fun ps -> let (ps,decls) = List.split ps in
                                     (P_list ps,List.flatten decls))
     ; p_cons           = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls'))
+    ; p_string_append  = (fun ((p1,decls1),(p2,decls2)) -> (P_string_append (p1,p2), decls1 @ decls2))
     ; p_aux            = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot))
     ; fP_aux           = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls))
     ; fP_Fpat          = (fun (id,(pat,decls)) -> (FP_Fpat (id,pat),decls))
@@ -1072,6 +1074,8 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
   | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats))
   | P_list pats -> rewrap (E_list (List.map pat_to_exp pats))
   | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps))
+  | P_string_append (p,ps) -> raise (Reporting_basic.err_unreachable l
+      "pat_to_exp not implemented for P_string_append")
 and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
   FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
 
@@ -1160,6 +1164,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
 | P_app (_,pats) | P_tup pats | P_list pats ->
     List.exists contains_bitvector_pat pats
 | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps
+| P_string_append (p1,p2) -> contains_bitvector_pat p1 || contains_bitvector_pat p2
 | P_record (fpats,_) ->
     List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats
 
@@ -1188,6 +1193,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
     ; p_cons           = (fun (p,ps) -> P_cons (p false, ps false))
+    ; p_string_append  = (fun (p1,p2) -> P_string_append (p1 false, p2 false))
     ; p_aux =
         (fun (pat,annot) contained_in_p_as ->
           let env = env_of_annot annot in
@@ -1342,6 +1348,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
                                     (P_list ps, flatten_guards_decls gdls))
     ; p_cons           = (fun ((p,gdls),(p',gdls')) ->
                           (P_cons (p,p'), flatten_guards_decls [gdls;gdls']))
+    ; p_string_append  = (fun ((p1,gdls1),(p2,gdls2)) ->
+                          (P_string_append (p1,p2), flatten_guards_decls [gdls1;gdls2]))
     ; p_aux            = (fun ((pat,gdls),annot) ->
                            let env = env_of_annot annot in
                            let t = Env.base_typ_of env (typ_of_annot annot) in
@@ -2801,6 +2809,103 @@ let pexp_rewriters rewrite_pexp =
   rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) }
 
 
+let stringappend_counter = ref 0
+
+let rec rewrite_defs_pat_string_append =
+  let rec rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) =
+
+    (* utils *)
+    let (pat, _, _, _) = destruct_pexp pexp in
+    let env = pat_env_of pat in
+    let assert_false = mk_exp (E_assert (mk_exp (E_lit (mk_lit L_false)), mk_exp (E_lit (mk_lit (L_string "unreachable"))))) in
+    let construct_single_match match_on pattern maybe_expr =
+      let (true_exp, false_exp) =
+        match maybe_expr with
+        | Some expr -> expr, assert_false
+        | None -> (mk_exp (E_lit (mk_lit L_true))), (mk_exp (E_lit (mk_lit L_false)))
+      in
+      mk_exp (E_case (match_on, [mk_pexp (Pat_exp (pattern, true_exp));
+                                 mk_pexp (Pat_exp (mk_pat P_wild, false_exp))]))
+    in
+
+    (* merge cases of Pat_exp and Pat_when *)
+    let (P_aux (p_aux, p_annot), guards, expr) =
+      match pexp_aux with
+      | Pat_exp (pat, expr) -> (pat, [], expr)
+      | Pat_when (pat, guard, expr) -> (pat, [guard], expr)
+    in
+
+    let (new_pat, new_guards, new_expr) =
+      match (p_aux, p_annot) with
+     (*
+        "lit" ^^ pat2 => expr ---> s# if startswith(s#, "lit")
+                                        && match str_drop(s#, strlen("lit")) {
+                                             pat2 => true, _ => false
+                                           }
+                                   => match str_drop(s#, strlen("lit")) {
+                                        pat2 => expr
+                                      }
+      *)
+      | P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _), pat2), p_annot ->
+
+         (* common things *)
+         let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in
+         stringappend_counter := !stringappend_counter + 1;
+         let env = Env.add_local id (Immutable, string_typ) env in
+
+         (* construct drop expression -- string_drop(s#, strlen("lit")) *)
+         let drop_exp = mk_exp (E_app (mk_id "string_drop", [mk_exp (E_id id); mk_exp (E_app (mk_id "string_length", [mk_exp (E_lit lit)]))])) in
+
+         (* construct the two new guards *)
+         let guard1 = mk_exp (E_app (mk_id "string_startswith", [mk_exp (E_id id); mk_exp (E_lit lit)])) in
+         let guard2 = construct_single_match drop_exp (strip_pat pat2) None in
+
+         (* recurse into pat2 *)
+         let new_pat2_pexp = mk_pexp (Pat_exp (strip_pat pat2, strip_exp expr)) in
+         let new_pat2_pexp = check_case env (pat_typ_of pat2) new_pat2_pexp (typ_of expr) in
+         let new_pat2_pexp = rewrite_pexp new_pat2_pexp in
+         let new_pat2_pexp = strip_pexp new_pat2_pexp in
+
+         (* construct new match expr *)
+         let new_expr = mk_exp (E_case (drop_exp, [new_pat2_pexp])) in
+
+         (* construct final result. TODO FIXME: *way* too much type-checking/stripping/rechecking *)
+         (mk_pat (P_id id)), guard1 :: guard2 :: (List.map strip_exp guards), new_expr
+
+     (*
+        (builtin x) ^^ pat2 => expr ---> s# if match maybe_atoi s# {
+                                                 Some (n#, len#) =>
+                                                   match string_drop(s#, len#) {
+                                                     pat2 => true, _ => false
+                                                   }
+                                                 None => false
+                                               }
+                                         => let (x, len#) = match maybe_atoi s# {
+                                                              Some (n#, len#) => (n#, len#)
+                                                            } in
+                                            match string_drop(s#, len#) {
+                                              pat2 => expr
+                                            }
+      *)
+      | P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _), pat2), p_annot ->
+         assert false
+      | P_string_append _, _ ->
+         failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat (P_aux (p_aux, p_annot)))
+
+      | _ -> strip_pat (P_aux (p_aux, p_annot)), (List.map strip_exp guards), (strip_exp expr)
+    in
+
+    (* un-merge Pat_exp and Pat_when cases *)
+    let new_pexp = match new_guards with
+    | [] -> mk_pexp (Pat_exp (new_pat, new_expr))
+    | gs -> mk_pexp (Pat_when (new_pat, fold_guards gs, new_expr))
+    in
+    check_case env string_typ new_pexp (typ_of expr)
+
+  in
+  pexp_rewriters rewrite_pexp
+
+
 let rewrite_defs_pat_lits =
   let counter = ref 0 in
   let rewrite_pat guards = function
@@ -3213,6 +3318,7 @@ let rewrite_defs_lem = [
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
   ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
   ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
+  ("pat_string_append", rewrite_defs_pat_string_append);
   ("guarded_pats", rewrite_defs_guarded_pats);
   ("bitvector_exps", rewrite_bitvector_exps);
   (* ("register_ref_writes", rewrite_register_ref_writes); *)
@@ -3241,6 +3347,7 @@ let rewrite_defs_lem = [
 let rewrite_defs_ocaml = [
     (* ("undefined", rewrite_undefined); *)
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("pat_string_append", rewrite_defs_pat_string_append);
   ("pat_lits", rewrite_defs_pat_lits);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
@@ -3260,6 +3367,7 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("pat_string_append", rewrite_defs_pat_string_append);
   ("pat_lits", rewrite_defs_pat_lits);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
@@ -3277,6 +3385,7 @@ let rewrite_defs_c = [
 
 let rewrite_defs_interpreter = [
     ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+    ("pat_string_append", rewrite_defs_pat_string_append);
     ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
     ("tuple_assignments", rewrite_tuple_assignments);
     ("simple_assignments", rewrite_simple_assignments);
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 47acae88..34d34993 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -461,6 +461,12 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2
 
 let eq_string (str1, str2) = String.compare str1 str2 == 0
 
+let string_startswith (str1, str2) = String.compare (String.sub str1 0 (String.length str2)) str2 == 0
+
+let string_drop (str, n) = let n = Big_int.to_int n in String.sub str n (String.length str - n)
+
+let string_length str = String.length str
+
 let lt_int (x, y) = Big_int.less x y
 
 let set_slice (out_len, slice_len, out, n, slice) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 63fab70e..523802cc 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2471,6 +2471,16 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards
        | _ -> typ_error l "Cannot match cons pattern against non-list type"
      end
+  | P_string_append (pat1, pat2) ->
+     begin
+       let matcher = Env.expand_synonyms env typ in
+       match matcher with
+       | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 ->
+          let pat1, env, guards1 = bind_pat env pat1 typ in
+          let pat2, env, guards2 = bind_pat env pat2 typ in
+          annot_pat (P_string_append (pat1, pat2)) typ, env, guards1 @ guards2
+       | _ -> typ_error l "Cannot match string-append pattern against non-string type"
+     end
   | P_list pats ->
      begin
        match Env.expand_synonyms env typ with
@@ -2600,6 +2610,12 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      in
      let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in
      annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards
+  | P_string_append (pat1, pat2) ->
+     let typed_pat1, env, guards1 = infer_pat env pat1 in
+     let typed_pat2, env, guards2 = infer_pat env pat2 in
+     typ_equality l env (pat_typ_of typed_pat1) (string_typ);
+     typ_equality l env (pat_typ_of typed_pat2) (string_typ);
+     annot_pat (P_string_append (typed_pat1, typed_pat2)) string_typ, env, guards1 @ guards2
   | P_as (pat, id) ->
      let (typed_pat, env, guards) = infer_pat env pat in
      annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat),
@@ -3415,6 +3431,10 @@ and propagate_pat_effect_aux = function
      let p_pat1 = propagate_pat_effect pat1 in
      let p_pat2 = propagate_pat_effect pat2 in
      P_cons (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2)
+  | P_string_append (pat1, pat2) ->
+     let p_pat1 = propagate_pat_effect pat1 in
+     let p_pat2 = propagate_pat_effect pat2 in
+     P_string_append (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2)
   | P_as (pat, id) ->
      let p_pat = propagate_pat_effect pat in
      P_as (p_pat, id), effect_of_pat p_pat
diff --git a/src/value.ml b/src/value.ml
index 4b4f0865..4848721d 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -183,6 +183,18 @@ let value_eq_string = function
   | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2))
   | _ -> failwith "value eq_string"
 
+let value_string_startswith = function
+  | [v1; v2] -> V_bool (Sail_lib.string_startswith (coerce_string v1, coerce_string v2))
+  | _ -> failwith "value string_startswith"
+
+let value_string_drop = function
+  | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2))
+  | _ -> failwith "value string_drop"
+
+let value_string_length = function
+  | [v] -> V_int (coerce_string v |> Sail_lib.string_length |> Big_int.of_int)
+  | _ -> failwith "value string_length"
+
 let value_length = function
   | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int)
   | _ -> failwith "value length"
@@ -417,6 +429,9 @@ let primops =
       ("eq_list", value_eq_list);
       ("eq_bool", value_eq_bool);
       ("eq_string", value_eq_string);
+      ("string_startswith", value_string_startswith);
+      ("string_drop", value_string_drop);
+      ("string_length", value_string_length);
       ("eq_anything", value_eq_anything);
       ("length", value_length);
       ("subrange", value_subrange);