Define String, SConst, StringLit, and associated funcs

Translate CPure SConst only for z3.ml and smtsolver.ml
All other provers call failwith() or illegal() when translating

astsimp.ml

@@ -92,6 +92,7 @@ let rec new_string_of_typ (x:typ) : string = match x with
   | Bool          -> "bool"
   | Float         -> "float"
   | Int           -> "int"
+  | String        -> "string"
   | INFInt        -> "INFint"
   | Void          -> "void"
   | NUM          -> "NUM"
@@ -628,6 +629,7 @@ let rec seq_elim (e:C.exp):C.exp = match e with
   | C.Dprint _
   | C.FConst _
   | C.IConst _
+  | C.SConst _
   | C.Print _
   | C.Java _ -> e
   (*| C.ArrayAlloc a -> C.ArrayAlloc {a with (* An Hoa *)
@@ -3825,6 +3827,7 @@ and all_paths_return (e0 : I.exp) : bool =
   | I.FloatLit _ -> false
   | I.Finally b-> all_paths_return b.I.exp_finally_body
   | I.IntLit _ -> false
+  | I.StringLit _ -> false
   | I.Java _ -> false
   | I.Label (_,e)-> all_paths_return e
   | I.Member _ -> false
@@ -5911,6 +5914,8 @@ and trans_exp_x (prog : I.prog_decl) (proc : I.proc_decl) (ie : I.exp) : trans_e
     | I.Empty pos -> ((C.Unit pos), C.void_type)
     | I.IntLit { I.exp_int_lit_val = i; I.exp_int_lit_pos = pos } ->
       ((C.IConst { C.exp_iconst_val = i; C.exp_iconst_pos = pos; }), C.int_type)
+    | I.StringLit { I.exp_string_lit_val = i; I.exp_string_lit_pos = pos } ->
+      ((C.SConst { C.exp_sconst_val = i; C.exp_sconst_pos = pos; }), C.string_type)
     | I.Java { I.exp_java_code = jcode; I.exp_java_pos = pos } ->
       ((C.Java { C.exp_java_code = jcode; C.exp_java_pos = pos; }), C.void_type)
     | I.Member {
@@ -6808,6 +6813,7 @@ and trans_exp_x (prog : I.prog_decl) (proc : I.proc_decl) (ie : I.exp) : trans_e
 and default_value (t :typ) pos : C.exp =
   match t with
   | Int -> C.IConst { C.exp_iconst_val = 0; C.exp_iconst_pos = pos; }
+  | String -> C.SConst { C.exp_sconst_val = ""; C.exp_sconst_pos = pos; }
   | Bool ->
     C.BConst { C.exp_bconst_val = false; C.exp_bconst_pos = pos; }
   | Float ->
@@ -8767,6 +8773,7 @@ and trans_pure_exp_x (e0 : IP.exp) (tlist:spec_var_type_list) prog : CP.exp =
     CP.Level ((trans_var (v,p) tlist prog pos),pos)
   | IP.Ann_Exp (e, t, pos) -> trans_pure_exp_x e tlist prog
   | IP.IConst (c, pos) -> CP.IConst (c, pos)
+  | IP.SConst (s, pos) -> CP.SConst (s, pos)
   | IP.FConst (c, pos) -> CP.FConst (c, pos)
   | IP.Add (e1, e2, pos) -> CP.Add (trans_pure_exp_x e1 tlist prog, trans_pure_exp_x e2 tlist prog, pos)
   | IP.Subtract (e1, e2, pos) -> CP.Subtract (trans_pure_exp_x e1 tlist prog, trans_pure_exp_x e2 tlist prog, pos)
@@ -9644,6 +9651,7 @@ and rename_exp_x (ren:(ident*ident) list) (f:Iast.exp):Iast.exp =
     | Iast.Block b-> Iast.Block{b with Iast.exp_block_body = helper ren b.Iast.exp_block_body}
     | Iast.FloatLit _
     | Iast.IntLit _
+    | Iast.StringLit _
     | Iast.Java _
     | Iast.Null _
     | Iast.Break _
@@ -9776,7 +9784,7 @@ and case_rename_var_decls (f:Iast.exp) : (Iast.exp * ((ident*ident) list)) =  ma
     (Iast.Block { b with Iast.exp_block_body = fst (case_rename_var_decls b.Iast.exp_block_body)},[])
 
   | Iast.Continue _  | Iast.Debug _ | Iast.Dprint _ | Iast.Empty _
-  | Iast.FloatLit _  | Iast.IntLit _  | Iast.Java _  | Iast.BoolLit _
+  | Iast.FloatLit _  | Iast.IntLit _  | Iast.StringLit _  | Iast.Java _  | Iast.BoolLit _
   | Iast.Null _   | Iast.Unfold _  | Iast.Var _ | Iast.This _  | Iast.Time _
   | Iast.Break _ | Iast.Barrier _ -> (f,[])
   | Iast.CallNRecv b ->
@@ -9955,6 +9963,7 @@ and case_normalize_exp prog (h: (ident*primed) list) (p: (ident*primed) list)(f:
   | Iast.Empty _
   | Iast.FloatLit _
   | Iast.IntLit _
+  | Iast.StringLit _
   | Iast.Java _
   | Iast.BoolLit _
   | Iast.Null _
@@ -10884,6 +10893,7 @@ and irf_traverse_exp (cp: C.prog_decl) (exp: C.exp) (scc: C.IG.V.t list) : (C.ex
   | C.Dprint _
   | C.FConst _
   | C.IConst _
+  | C.SConst _
   | C.New _
   | C.Null _
   | C.EmptyArray _

cast.ml

@@ -419,6 +419,10 @@ and exp_iconst = {
   exp_iconst_val : int;
   exp_iconst_pos : loc }
 
+and exp_sconst = {
+  exp_sconst_val : string;
+  exp_sconst_pos : loc }
+
 and exp_new = {
   exp_new_class_name : ident;
   exp_new_parent_name : ident;
@@ -557,6 +561,7 @@ and exp = (* expressions keep their types *)
         *)
   | ICall of exp_icall
   | IConst of exp_iconst
+  | SConst of exp_sconst
   (*| ArrayAlloc of exp_aalloc *) (* An Hoa *)
   | New of exp_new
   | Null of loc
@@ -1090,6 +1095,7 @@ let transform_exp (e:exp) (init_arg:'b)(f:'b->exp->(exp* 'a) option)  (f_args:'b
       | FConst _
       | ICall _
       | IConst _
+      | SConst _
       (* | ArrayAlloc _ *) (* An Hoa *)
       | New _
       | Null _
@@ -1216,6 +1222,8 @@ let void_type = Void
 
 let int_type = Int
 
+let string_type = String
+
 let infint_type = INFInt
 
 let float_type = Float
@@ -1305,6 +1313,7 @@ let rec type_of_exp (e : exp) = match e with
   (*| FieldRead (t, _, _, _) -> Some t*)
   (*| FieldWrite _ -> Some Void*)
   | IConst _ -> Some int_type
+  | SConst _ -> Some string_type
   (* An Hoa *)
   (* | ArrayAlloc ({exp_aalloc_etype = t;
      		  exp_aalloc_dimension = _;
@@ -2162,6 +2171,7 @@ and callees_of_exp (e0 : exp) : ident list = match e0 with
             exp_icall_arguments = _;
             exp_icall_pos = _}) -> [unmingle_name n] (* to be fixed: look up n, go down recursively *)
   | IConst _ -> []
+  | SConst _ -> []
   (*| ArrayAlloc _ -> []*)
   | New _ -> []
   | Null _ -> []
@@ -2432,6 +2442,7 @@ and exp_to_check (e:exp) :bool = match e with
   | Assign _
   | ICall _
   | IConst _
+  | SConst _
   | While _
   | This _
   | Var _
@@ -2459,6 +2470,7 @@ let rec pos_of_exp (e:exp) :loc = match e with
   | FConst b -> b.exp_fconst_pos
   | ICall b -> b.exp_icall_pos
   | IConst b -> b.exp_iconst_pos
+  | SConst b -> b.exp_sconst_pos
   | Print (_,b) -> b
   | Seq b -> b.exp_seq_pos
   | VarDecl b -> b.exp_var_decl_pos
@@ -2996,6 +3008,7 @@ let exp_fv (e:exp) =
     | FConst _ -> Some ac
     | ICall b -> Some (b.exp_icall_receiver::b.exp_icall_arguments@ac)
     | IConst _ -> Some ac
+    | SConst _ -> Some ac
     | New b -> Some ((List.map snd b.exp_new_arguments)@ac)
     | Null _ -> Some ac
     | EmptyArray _ -> Some ac

cformula.ml

@@ -18587,6 +18587,7 @@ let elim_prm e =
   let f_e e = match e with
     | CP.Null _
     | CP.IConst _
+    | CP.SConst _
     | CP.AConst _
     | CP.Tsconst _
     | CP.FConst _

cilparser.ml

@@ -155,6 +155,7 @@ let rec loc_of_iast_exp (e: Iast.exp) : VarGen.loc =
   | Iast.FloatLit e -> e.Iast.exp_float_lit_pos
   | Iast.Finally e -> e.Iast.exp_finally_pos
   | Iast.IntLit e -> e.Iast.exp_int_lit_pos
+  | Iast.StringLit e -> e.Iast.exp_string_lit_pos
   | Iast.Java e -> e.Iast.exp_java_pos
   | Iast.Label (_, e1) -> loc_of_iast_exp e1
   | Iast.Member e -> e.Iast.exp_member_pos
@@ -1389,7 +1390,7 @@ and translate_constant (c: Cil.constant) (lopt: Cil.location option) : Iast.exp
   let pos = match lopt with None -> no_pos | Some l -> translate_location l in
   match c with
   | Cil.CInt64 (i, _, _) -> Iast.mkIntLit (Int64.to_int i) pos
-  | Cil.CStr s -> report_error pos "TRUNG TODO: Handle Cil.CStr later!"
+  | Cil.CStr s -> Iast.mkStringLit s pos
   | Cil.CWStr _ -> report_error pos "TRUNG TODO: Handle Cil.CWStr later!"
   (*| Cil.CChr _ -> report_error pos "TRUNG TODO: Handle Cil.CChr later!"*)
   | Cil.CChr c -> Iast.mkIntLit (Char.code c) pos
@@ -2290,6 +2291,8 @@ and translate_hip_exp_x (exp: Iast.exp) pos : Iast.exp =
       Iast.mkMember addr_var ["deref"] None pos*)
     | Ipure.IConst (i, pos) ->
       Ipure.IConst (i, pos)
+    | Ipure.SConst (s, pos) ->
+      Ipure.SConst (s, pos)
     | Ipure.FConst (f, pos) ->
       Ipure.FConst (f, pos)
     | Ipure.AConst (ha, pos) ->

coq.ml

@@ -29,6 +29,7 @@ let rec coq_of_typ = function
   | Bool          -> "int"
   | Float         -> "float"	(* all types will be ints. *)
   | Int | INFInt  -> "int"
+  | String -> illegal_format ("coq_of_typ: String type not supported for Coq")
   | AnnT          -> "int"
   | Void          -> "unit" 	(* all types will be ints. *)
   | BagT t		   -> "("^(coq_of_typ t) ^") set"
@@ -85,6 +86,7 @@ and coq_of_exp e0 =
   | CP.Null _ -> "0"
   | CP.Var (sv, _) -> coq_of_spec_var sv
   | CP.IConst (i, _) -> string_of_int i
+  | CP.SConst (s, _) -> failwith ("coq_of_exp: String cannot be handled")
   | CP.Tsconst _ -> failwith ("tsconst not supported in coq, should have already been handled")
   | CP.Bptriple _ | CP.Tup2 _ ->  illegal_format "coq_of_exp : bptriple/Tup2 cannot be handled"
   | CP.AConst (i, _) -> string_of_heap_ann i

cprinter.ml

@@ -862,6 +862,7 @@ let rec pr_formula_exp (e:P.exp) =
   | P.Var (x, l) -> fmt_string (string_of_spec_var x) (* fmt_string (string_of_typed_spec_var x) *)
   | P.Level (x, l) -> fmt_string ("level(" ^ (string_of_spec_var x) ^ ")")
   | P.IConst (i, l) -> fmt_int i
+  | P.SConst (s, l) -> fmt_string s
   | P.AConst (i, l) -> fmt_string (string_of_heap_ann i)
   | P.InfConst (i,l) -> let r = "\\inf" in fmt_string r
   | P.NegInfConst (i,l) -> let r = "~\\inf" in fmt_string r
@@ -4726,6 +4727,7 @@ let rec string_of_exp = function
   (*| FieldRead (_, (v, _), (f, _), _) -> v ^ "." ^ f*)
   (*| FieldWrite ((v, _), (f, _), r, _) -> v ^ "." ^ f ^ " = " ^ r*)
   | IConst ({exp_iconst_val = i; exp_iconst_pos = l}) -> string_of_int i
+  | SConst ({exp_sconst_val = s; exp_sconst_pos = l}) -> s
   | New ({exp_new_class_name = id;
           exp_new_arguments = idl;
           exp_new_pos = l}) ->
@@ -5248,6 +5250,7 @@ let rec html_of_formula_exp e =
   | P.Var (x, l) -> html_of_spec_var x
   | P.Level (x, l) -> "<level>" ^ html_of_spec_var x ^ "</level>"
   | P.IConst (i, l) -> string_of_int i
+  | P.SConst (s, l) -> s
   | P.FConst (f, l) -> string_of_float f
   | P.AConst (f, l) -> string_of_heap_ann f
   | P.Tsconst(f, l) -> Tree_shares.Ts.string_of f

cpure.ml

@@ -311,6 +311,7 @@ and exp =
   | Var of (spec_var * loc)
   | Level of (spec_var * loc) (*represent locklevel of a lock spec_var*)
   | IConst of (int * loc)
+  | SConst of (string * loc)
   | FConst of (float * loc)
   | AConst of (heap_ann * loc)
   | InfConst of (ident * loc)
@@ -1319,6 +1320,7 @@ let rec get_exp_type (e : exp) : typ =
   | Var (SpecVar (t, _, _), _) -> t
   | Level _ -> Globals.level_data_typ
   | IConst _ -> Int
+  | SConst _ -> String
   | InfConst _ -> Int
   | NegInfConst _ -> Int
   | FConst _ -> Float
@@ -1585,6 +1587,7 @@ and afv (af : exp) : spec_var list =
   match af with
   | Null _
   | IConst _
+  | SConst _
   | AConst _
   | InfConst _
   | NegInfConst _
@@ -2346,7 +2349,7 @@ and is_exp_arith (e:exp) : bool=
   match e with
   | Var (sv,pos) ->        (*waitlevel is a kind of bag constraints*)
     if (name_of_spec_var sv = Globals.waitlevel_name) then false else true
-  | Null _  | IConst _ | AConst _ | InfConst _ | NegInfConst _ | FConst _
+  | Null _  | IConst _ | SConst _ | AConst _ | InfConst _ | NegInfConst _ | FConst _
   | Level _ -> true
   | Add (e1,e2,_)  | Subtract (e1,e2,_)  | Mult (e1,e2,_)
   | Div (e1,e2,_)  | Max (e1,e2,_)  | Min (e1,e2,_) -> (is_exp_arith e1) && (is_exp_arith e2)
@@ -3206,6 +3209,7 @@ let foldr_exp (e:exp) (arg:'a) (f:'a->exp->(exp * 'b) option)
       | Var _
       | Level _
       | IConst _
+      | SConst _
       | InfConst _
       | NegInfConst _
       | AConst _
@@ -3334,6 +3338,7 @@ let rec transform_exp f e  =
     | Var _
     | Level _
     | IConst _
+    | SConst _
     | AConst _
     | InfConst _
     | NegInfConst _
@@ -4050,6 +4055,7 @@ and pos_of_exp (e : exp) = match e with
   | Var (_, p)
   | Level (_, p)
   | IConst (_, p)
+  | SConst (_, p)
   | InfConst (_,p)
   | NegInfConst (_,p)
   | AConst (_, p)
@@ -4685,7 +4691,7 @@ and subs_one sst v =
   in helper sst v
 
 and e_apply_subs sst e = match e with
-  | Null _ | IConst _ | FConst _ | AConst _ | InfConst _ | NegInfConst _ |Tsconst _ -> e
+  | Null _ | IConst _ | SConst _ | FConst _ | AConst _ | InfConst _ | NegInfConst _ |Tsconst _ -> e
   | Bptriple ((ec,et,ea),pos) ->
     Bptriple ((subs_one sst ec,
                subs_one sst et,
@@ -4744,7 +4750,7 @@ and b_subst (zip: (spec_var * spec_var) list) (bf:b_formula) :b_formula =
 and e_apply_one_spec_var (fr, t) sv = if eq_spec_var sv fr then t else sv
 
 and e_apply_one (fr, t) e = match e with
-  | Null _ | IConst _ | InfConst _ | NegInfConst _ | FConst _ | AConst _ | Tsconst _ -> e
+  | Null _ | IConst _ | SConst _ | InfConst _ | NegInfConst _ | FConst _ | AConst _ | Tsconst _ -> e
   | Bptriple ((ec,et,ea),pos) ->
     Bptriple ((e_apply_one_spec_var (fr, t) ec,
                e_apply_one_spec_var (fr, t) et,
@@ -4878,6 +4884,7 @@ and a_apply_par_term (sst : (spec_var * exp) list) e =
   match e with
   | Null _
   | IConst _
+  | SConst _
   | InfConst _
   | NegInfConst _
   | FConst _
@@ -5001,6 +5008,7 @@ and b_apply_one_term ((fr, t) : (spec_var * exp)) bf =
 and a_apply_one_term ((fr, t) : (spec_var * exp)) e = match e with
   | Null _
   | IConst _
+  | SConst _
   | AConst _
   | InfConst _
   | NegInfConst _
@@ -5057,6 +5065,7 @@ and a_apply_one_term_selective variance ((fr, t) : (spec_var * exp)) e : (bool*e
   and helper crt_var e = match e with
     | Null _
     | IConst _
+    | SConst _
     | InfConst _
     | NegInfConst _
     | FConst _
@@ -6608,7 +6617,7 @@ and b_apply_one_exp (fr, t) bf =
   in (npf,il)
 
 and e_apply_one_exp (fr, t) e = match e with
-  | Null _ | IConst _ | InfConst _ | NegInfConst _ | FConst _| AConst _ | Tsconst _ -> e
+  | Null _ | IConst _ | SConst _ | InfConst _ | NegInfConst _ | FConst _| AConst _ | Tsconst _ -> e
   | Bptriple _ -> e
   | Var (sv, pos) -> if eq_spec_var sv fr then t else e
   | Level (sv, pos) -> if eq_spec_var sv fr then t else e
@@ -6855,6 +6864,7 @@ and of_interest (e1:exp) (e2:exp) (interest_vars:spec_var list):bool =
     | Var _
     | Level _
     | IConst _
+    | SConst _
     | InfConst _
     | NegInfConst _
     | AConst _
@@ -7065,6 +7075,7 @@ and simp_mult_x (e : exp) :  exp =
     |  ListHead (_, l)
     |  ListLength (_, l)
     |  Func (_, _, l)
+    |  SConst (_, l)
     | Template { templ_pos = l; }
     |  ArrayAt (_, _, l) ->
       match m with | None -> e0 | Some c ->  Mult (IConst (c, l), e0, l)
@@ -7093,6 +7104,7 @@ and split_sums_x (e :  exp) : (( exp option) * ( exp option)) =
     else
       (* if v < 0 then *)
       (None, (Some ( IConst (- v, l))))
+  |  SConst (v, l) -> ((Some e), None)
   (* else (None, None) *)
   | FConst (v, l) ->
     if v >= 0.0 then
@@ -7234,6 +7246,7 @@ and purge_mult_x (e :  exp):  exp = match e with
   |  Var _
   |  Level _
   |  IConst _
+  |  SConst _
   |  AConst _
   | InfConst _
   | NegInfConst _
@@ -7596,6 +7609,7 @@ let rec get_head e = match e with
   | Var (v,_) -> name_of_spec_var v
   | Level (v,_) -> name_of_spec_var v
   | IConst (i,_)-> string_of_int i
+  | SConst (s,_)-> s
   | InfConst(i,_) -> i
   | NegInfConst(i,_) -> i
   | FConst (f,_) -> string_of_float f
@@ -7657,7 +7671,7 @@ and norm_exp (e:exp) =
   (* let () = print_string "\n !!!!!!!!!!!!!!!! norm exp aux \n" in *)
   let rec helper e = match e with
     | Var _
-    | Null _ | IConst _ | InfConst _ | NegInfConst _ | FConst _ | AConst _ | Tsconst _
+    | Null _ | IConst _ | SConst _ | InfConst _ | NegInfConst _ | FConst _ | AConst _ | Tsconst _
     | Bptriple _
     | Level _ -> e
     | Tup2 ((e1,e2),l) -> Tup2 ((helper e1,helper e2),l)
@@ -10178,6 +10192,7 @@ let compute_instantiations_x pure_f v_of_int avail_v =
 
     and helper (e:exp) (rhs_e:exp) :exp = match e with
       | IConst _
+      | SConst _
       | FConst _
       | InfConst _
       | NegInfConst _