Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Define String, SConst, StringLit, and associated funcs #29

Closed
wants to merge 5 commits into from
Closed

Define String, SConst, StringLit, and associated funcs #29

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
b4777ef
Define String, SConst, StringLit, and associated funcs
zhengqunkoo Jun 17, 2020
9ef31b7
Translate TInt(IChar), autogenerate char_star with char field
zhengqunkoo Jun 18, 2020
59a8606
Expand subtyping, allow assignments `char *s = "..."`
zhengqunkoo Jun 18, 2020
5aaba1e
Support checking of SConst expressions
zhengqunkoo Jun 18, 2020
60392cb
Try to force variable `s` to only be type `String`
zhengqunkoo Jun 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion astsimp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 _
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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 _
Expand Down Expand Up @@ -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 _
Expand Down
13 changes: 13 additions & 0 deletions cast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 _
Expand Down Expand Up @@ -1216,6 +1222,8 @@ let void_type = Void

let int_type = Int

let string_type = String

let infint_type = INFInt

let float_type = Float
Expand Down Expand Up @@ -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 = _;
Expand Down Expand Up @@ -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 _ -> []
Expand Down Expand Up @@ -2432,6 +2442,7 @@ and exp_to_check (e:exp) :bool = match e with
| Assign _
| ICall _
| IConst _
| SConst _
| While _
| This _
| Var _
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions cformula.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _
Expand Down
7 changes: 5 additions & 2 deletions cilparser.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -1285,7 +1286,7 @@ and translate_typ_x (t: Cil.typ) pos : Globals.typ =
match t with
| Cil.TVoid _ -> Globals.Void
| Cil.TInt (Cil.IBool, _) -> Globals.Bool
(*| Cil.TInt (Cil.IChar, _) -> Globals.Named "char"*)
| Cil.TInt (Cil.IChar, _) -> Globals.Named "char"
| Cil.TInt _ -> Globals.Int
| Cil.TFloat _ -> Globals.Float
| Cil.TPtr (ty, _) -> (
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) ->
Expand Down
2 changes: 2 additions & 0 deletions coq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions cprinter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}) ->
Expand Down Expand Up @@ -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
Expand Down
Loading