Skip to content

Commit ac87d38

Browse files
author
Ronald Judin
committed
Analysis has tracking set, params are a list
1 parent d663309 commit ac87d38

File tree

6 files changed

+110
-133
lines changed

6 files changed

+110
-133
lines changed

‎src/analyses/base.ml‎

Lines changed: 2 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -2760,33 +2760,8 @@ struct
27602760
| _ -> st
27612761
end
27622762
(* TODO: Rethink OCamlParam's placement *)
2763-
| OCamlParam {param1; param2; param3; param4; param5}, _ ->
2764-
begin match param1 with
2765-
| Some p1 ->
2766-
let _ = eval_rv ~man st p1 in
2767-
begin match param2 with
2768-
| Some p2 ->
2769-
let _ = eval_rv ~man st p2 in
2770-
begin match param3 with
2771-
| Some p3 ->
2772-
let _ = eval_rv ~man st p3 in
2773-
begin match param4 with
2774-
| Some p4 ->
2775-
let _ = eval_rv ~man st p4 in
2776-
begin match param5 with
2777-
| Some p5 ->
2778-
let _ = eval_rv ~man st p5 in
2779-
st
2780-
| _ -> st
2781-
end
2782-
| _ -> st
2783-
end
2784-
| _ -> st
2785-
end
2786-
| _ -> st
2787-
end
2788-
| _ -> st
2789-
end
2763+
| OCamlParam params, _ ->
2764+
List.fold_left (fun acc param -> let _ = eval_rv ~man acc param in acc) st params
27902765
| Calloc { count = n; size }, _ ->
27912766
begin match lv with
27922767
| Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *)

‎src/analyses/ocaml.ml‎

Lines changed: 62 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -27,32 +27,42 @@ struct
2727
let name () = "ocaml"
2828
module D =
2929
struct
30-
(* The first set contains variables of type value that are definitely in order. The second contains definitely registered variables. *)
31-
module P = Lattice.Prod (VarinfoSet) (VarinfoSet)
30+
(* The first set contains variables of type value that are definitely in order. The second contains definitely registered variables. The third contains variables the analysis tracks. *)
31+
module P = Lattice.Prod3 (VarinfoSet) (VarinfoSet) (VarinfoSet)
3232
include P
3333

34-
let empty () = (VarinfoSet.empty (), VarinfoSet.empty ())
34+
let empty () = (VarinfoSet.empty (), VarinfoSet.empty (), VarinfoSet.empty ())
3535

3636
(* After garbage collection, the second set is written to the first set *)
37-
let after_gc (accounted, registered) = (registered, registered)
37+
let after_gc (accounted, registered, tracked) = (registered, registered, tracked)
3838

39-
let mem_a v (accounted, registered) =
39+
(* Untracked variables are always fine. *)
40+
let mem_a v (accounted, registered, tracked) =
4041
VarinfoSet.mem v accounted
4142

42-
let mem_r v (accounted, registered) =
43+
let mem_r v (accounted, registered, tracked) =
4344
VarinfoSet.mem v registered
4445

45-
let add_a v (accounted, registered) =
46-
(VarinfoSet.add v accounted, registered)
46+
let mem_t v (accounted, registered, tracked) =
47+
VarinfoSet.mem v tracked
4748

48-
let add_r v (accounted, registered) =
49-
(accounted, VarinfoSet.add v registered)
49+
let add_a v (accounted, registered, tracked) =
50+
(VarinfoSet.add v accounted, registered, tracked)
5051

51-
let remove_a v (accounted, registered) =
52-
(VarinfoSet.remove v accounted, registered)
52+
let add_r v (accounted, registered, tracked) =
53+
(accounted, VarinfoSet.add v registered, tracked)
5354

54-
let remove_r v (accounted, registered) =
55-
(accounted, VarinfoSet.remove v registered)
55+
let add_t v (accounted, registered, tracked) =
56+
(accounted, registered, VarinfoSet.add v tracked)
57+
58+
let remove_a v (accounted, registered, tracked) =
59+
(VarinfoSet.remove v accounted, registered, tracked)
60+
61+
let remove_r v (accounted, registered, tracked) =
62+
(accounted, VarinfoSet.remove v registered, tracked)
63+
64+
let remove_t v (accounted, registered, tracked) =
65+
(accounted, registered, VarinfoSet.remove v tracked)
5666
end
5767
module C = Printable.Unit
5868

@@ -79,11 +89,33 @@ struct
7989
and lval_accounted_for state = function
8090
| (Var v, _) ->
8191
(* Checks whether variable v is accounted for *) (*false*)
82-
if D.mem_a v state then true else let _ = M.warn "Value %a might be garbage collected" CilType.Varinfo.pretty v in false
92+
if D.mem_a v state || not (D.mem_t v state) then true else let _ = M.warn "Value %a might be garbage collected" CilType.Varinfo.pretty v in false
8393
| _ ->
8494
(* The Gemara asks: is using an offset safe for the expression? The Gemara answers: by default, no. We assume our language has no pointers *)
8595
false
8696

97+
(** Determines whether an expression [e] has parts in the OCaml heap, given a [state]. *)
98+
let rec exp_tracked (state:D.t) (e:Cil.exp) = match e with
99+
(* Recurse over the structure in the expression, returning true if some varinfo appearing in the expression is tracked *)
100+
| AddrOf v
101+
| StartOf v
102+
| Lval v -> lval_tracked state v
103+
| BinOp (_,e1,e2,_) -> exp_tracked state e1 || exp_tracked state e2
104+
| Real e
105+
| Imag e
106+
| SizeOfE e
107+
| AlignOfE e
108+
| CastE (_,e)
109+
| UnOp (_,e,_) -> exp_tracked state e
110+
| SizeOf _ | SizeOfStr _ | Const _ | AlignOf _ | AddrOfLabel _ -> false
111+
| Question (b, t, f, _) -> exp_tracked state b || exp_tracked state t || exp_tracked state f
112+
and lval_tracked state = function
113+
| (Var v, _) ->
114+
(* Checks whether variable v is tracked *)
115+
D.mem_t v state
116+
| _ ->
117+
false
118+
87119
(* transfer functions *)
88120

89121
(** Handles assignment of [rval] to [lval]. *)
@@ -92,8 +124,10 @@ struct
92124
match lval with
93125
| Var v,_ ->
94126
(* If lval is of type value, checks whether rval is accounted for, handles assignment to v accordingly *) (* state *)
95-
if exp_accounted_for state rval then D.add_a v state
96-
else D.remove_a v state
127+
if exp_accounted_for state rval then
128+
if exp_tracked state rval then D.add_a v (D.add_t v state)
129+
else D.add_a v (D.remove_t v state)
130+
else let _ = M.info "The above is being assigned" in D.remove_a v (D.add_t v state)
97131
| _ -> state
98132

99133
(** Handles conditional branching yielding truth value [tv]. *)
@@ -104,9 +138,9 @@ struct
104138
(** Handles going from start node of function [f] into the function body of [f].
105139
Meant to handle e.g. initializiation of local variables. *)
106140
let body ctx (f:fundec) : D.t =
107-
(* The (non-formals) locals are initially accounted for *)
141+
(* The (non-formals) locals are tracked and initially accounted for *)
108142
let state = ctx.local in
109-
List.fold_left (fun st v -> D.add_a v st) state f.sformals
143+
List.fold_left (fun st v -> D.add_a v (D.add_t v st)) state f.sformals
110144

111145
(** Handles the [return] statement, i.e. "return exp" or "return", in function [f]. *)
112146
let return ctx (exp:exp option) (f:fundec) : D.t =
@@ -115,6 +149,7 @@ struct
115149
| Some e ->
116150
(* Checks that value returned is accounted for. *)
117151
(* Return_varinfo is used in place of a "real" variable. *)
152+
(* TODO: Consider how the return_varinfo needs to be tracked. *)
118153
(* state *)
119154
if exp_accounted_for state e then D.add_a return_varinfo state
120155
else let _ = M.warn "Value returned might be garbage collected" in D.remove_a return_varinfo state
@@ -155,6 +190,7 @@ struct
155190
let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
156191
let caller_state = ctx.local in
157192
(* Records whether lval was accounted for. *) (* caller_state *)
193+
(* TODO: Consider how the return_varinfo needs to be tracked. *)
158194
match lval with (* The variable returned is played by return_varinfo *)
159195
| Some (Var v, _) -> if D.mem_a return_varinfo callee_local then D.add_a v caller_state
160196
else let _ = M.warn "Returned value may be garbage-collected" in D.remove_a v caller_state
@@ -170,54 +206,14 @@ struct
170206
(* caller_state *)
171207
let desc = LibraryFunctions.find f in
172208
match desc.special arglist with
209+
(* Variables are registered with a Param macro. *)
173210
| OCamlParam params ->
174-
(* Variables are registered with a Param macro. *)
175-
(* TODO: Which pattern below do the params in fact match? Does it vary? *)
176-
(* The function extract_varinfo is from AI - the code can be shortened when we know what the params are. *)
177-
let rec extract_varinfo (e: Cil.exp): varinfo option = match e with
178-
(* Direct variable lvalue *)
179-
| Lval (Var v, _) -> Some v
180-
(* Dereferenced pointer - try to extract from inner expression *)
181-
| Lval (Mem inner, _) -> extract_varinfo inner
182-
(* Address of variable *)
183-
| AddrOf (Var v, _) -> Some v (* TODO: Maybe this is the only thing a param can be. *)
184-
(* Address of dereferenced - try to extract from inner *)
185-
| AddrOf (Mem inner, _) -> extract_varinfo inner
186-
(* Array start of variable *)
187-
| StartOf (Var v, _) -> Some v
188-
(* Array start of dereferenced *)
189-
| StartOf (Mem inner, _) -> extract_varinfo inner
190-
(* Type cast - extract from inner expression *)
191-
| CastE (_, inner) -> extract_varinfo inner
192-
(* Unary operations - extract from operand *)
193-
| UnOp (_, inner, _) -> extract_varinfo inner
194-
(* Real/imaginary parts *)
195-
| Real inner | Imag inner -> extract_varinfo inner
196-
(* Binary operations - try both operands *)
197-
| BinOp (_, e1, e2, _) ->
198-
(match extract_varinfo e1 with
199-
| Some v -> Some v
200-
| None -> extract_varinfo e2)
201-
(* Size and alignment - may contain var info in the type *)
202-
| SizeOfE inner | AlignOfE inner -> extract_varinfo inner
203-
(* Constants, SizeOf, AlignOf, SizeOfStr, AddrOfLabel - no varinfo *)
204-
| Const _ | SizeOf _ | AlignOf _ | SizeOfStr _ | AddrOfLabel _ -> None
205-
(* Question conditional *)
206-
| Question (cond, e1, e2, _) ->
207-
(match extract_varinfo cond with
208-
| Some v -> Some v
209-
| None ->
210-
(match extract_varinfo e1 with
211-
| Some v -> Some v
212-
| None -> extract_varinfo e2))
213-
in
214-
List.fold_left (fun state param ->
215-
match param with
216-
| Some e ->
217-
(match extract_varinfo e with
218-
| Some v -> D.add_r v state
219-
| None -> state)
220-
| None -> state) caller_state [params.param1; params.param2; params.param3; params.param4; params.param5]
211+
List.fold_left (fun state param -> let _ = M.info "We reach here" in
212+
match param with
213+
| AddrOf (Var v, _) -> let _ = M.info "Address of" in
214+
D.add_r v state
215+
| _ -> state
216+
) caller_state params
221217
| OCamlAlloc size_exp ->
222218
(* Garbage collection may trigger here and overwrite unregistered variables *)
223219
let _ = M.debug "Garbage collection triggers" in (match lval with

‎src/util/library/libraryDesc.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@ type special =
4848
| Alloca of Cil.exp
4949
| Malloc of Cil.exp
5050
| OCamlAlloc of Cil.exp
51-
(* TODO: Rethink OCamlParam's placement and make the params a list. *)
52-
| OCamlParam of { param1: Cil.exp option; param2: Cil.exp option; param3: Cil.exp option; param4: Cil.exp option; param5: Cil.exp option; }
51+
(* TODO: Rethink OCamlParam's placement. *)
52+
| OCamlParam of Cil.exp list
5353
| Calloc of { count: Cil.exp; size: Cil.exp; }
5454
| Realloc of { ptr: Cil.exp; size: Cil.exp; }
5555
| Free of Cil.exp

‎src/util/library/libraryFunctions.ml‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
162162
("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
163163
("atexit", unknown [drop "function" [if_ (fun () -> not (get_bool "sem.atexit.ignore")) s]]);
164164
("atoi", unknown [drop "nptr" [r]]);
165+
("atof", unknown [drop "nptr" [r]]); (* TODO: Rethink atof's position in this list. *)
165166
("atol", unknown [drop "nptr" [r]]);
166167
("atoll", unknown [drop "nptr" [r]]);
167168
("setlocale", unknown [drop "category" []; drop "locale" [r]]);
@@ -1246,12 +1247,12 @@ let ocaml_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
12461247
("caml_copy_double", special [drop "nptr" []] (OCamlAlloc (GoblintCil.integer 1)));
12471248
(* Eeskuju: ("malloc", special [__ "size" []] @@ fun size -> Malloc size); *)
12481249
("caml_alloc_small", special [__ "wosize" []; __ "tag" []] @@ fun wosize tag -> OCamlAlloc wosize);
1249-
("__goblint_caml_param0", special [] @@ OCamlParam {param1 = None; param2 = None; param3 = None; param4 = None; param5 = None});
1250-
("__goblint_caml_param1", special [__ "param" []] @@ fun param -> OCamlParam {param1 = Some param; param2 = None; param3 = None; param4 = None; param5 = None});
1251-
("__goblint_caml_param2", special [__ "param1" []; __ "param2" []] @@ fun param1 param2 -> OCamlParam {param1 = Some param1; param2 = Some param2; param3 = None; param4 = None; param5 = None});
1252-
("__goblint_caml_param3", special [__ "param1" []; __ "param2" []; __ "param3" []] @@ fun param1 param2 param3 -> OCamlParam {param1 = Some param1; param2 = Some param2; param3 = Some param3; param4 = None; param5 = None});
1253-
("__goblint_caml_param4", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []] @@ fun param1 param2 param3 param4 -> OCamlParam {param1 = Some param1; param2 = Some param2; param3 = Some param3; param4 = Some param4; param5 = None});
1254-
("__goblint_caml_param5", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []; __ "param5" []] @@ fun param1 param2 param3 param4 param5 -> OCamlParam {param1 = Some param1; param2 = Some param2; param3 = Some param3; param4 = Some param4; param5 = Some param5});
1250+
("__goblint_caml_param0", special [] @@ OCamlParam []);
1251+
("__goblint_caml_param1", special [__ "param" []] @@ fun param -> OCamlParam [param]);
1252+
("__goblint_caml_param2", special [__ "param1" []; __ "param2" []] @@ fun param1 param2 -> OCamlParam [param1; param2]);
1253+
("__goblint_caml_param3", special [__ "param1" []; __ "param2" []; __ "param3" []] @@ fun param1 param2 param3 -> OCamlParam [param1; param2; param3]);
1254+
("__goblint_caml_param4", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []] @@ fun param1 param2 param3 param4 -> OCamlParam [param1; param2; param3; param4]);
1255+
("__goblint_caml_param5", special [__ "param1" []; __ "param2" []; __ "param3" []; __ "param4" []; __ "param5" []] @@ fun param1 param2 param3 param4 param5 -> OCamlParam [param1; param2; param3; param4; param5]);
12551256
]
12561257
[@@coverage off]
12571258

‎tests/regression/90-ocaml/02-floatops.c‎

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "UNARY_OP" --set "mainfun[+]" "BINARY_OP" --set "mainfun[+]" "atof_double" --set "mainfun[+]" "atof_float" --set "mainfun[+]" "max_float" --set "mainfun[+]" "smallest_float" --set "mainfun[+]" "pi_float" --disable warn.imprecise --set "exp.extraspecials[+]" printInt
1+
// PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "sqrt_double" --set "mainfun[+]" "sqrt_float" --set "mainfun[+]" "acos_double" --set "mainfun[+]" "acos_float" --set "mainfun[+]" "asin_double" --set "mainfun[+]" "asin_float" --set "mainfun[+]" "atan_double" --set "mainfun[+]" "atan_float" --set "mainfun[+]" "cos_double" --set "mainfun[+]" "cos_float" --set "mainfun[+]" "sin_double" --set "mainfun[+]" "sin_float" --set "mainfun[+]" "tan_double" --set "mainfun[+]" "tan_float" --set "mainfun[+]" "add_double" --set "mainfun[+]" "add_float" --set "mainfun[+]" "sub_double" --set "mainfun[+]" "sub_float" --set "mainfun[+]" "mul_double" --set "mainfun[+]" "mul_float" --set "mainfun[+]" "div_double" --set "mainfun[+]" "div_float" --set "mainfun[+]" "atof_double" --set "mainfun[+]" "atof_float" --set "mainfun[+]" "max_float" --set "mainfun[+]" "smallest_float" --set "mainfun[+]" "pi_float" --disable warn.imprecise --set "exp.extraspecials[+]" printInt
22

33
// Code from stubs.c in src/common/cdomains/floatOps that should be correct despite missing CAMLparam, as discussed in https://github.com/goblint/analyzer/issues/1371.
44

@@ -69,20 +69,20 @@ static void change_round_mode(int mode)
6969
/* No need to use CAMLreturn because we don't use CAMLparam. */ \
7070
}
7171

72-
UNARY_OP(sqrt, double, sqrt);
73-
UNARY_OP(sqrt, float, sqrtf);
74-
UNARY_OP(acos, double, acos);
75-
UNARY_OP(acos, float, acosf);
76-
UNARY_OP(asin, double, asin);
77-
UNARY_OP(asin, float, asinf);
78-
UNARY_OP(atan, double, atan);
79-
UNARY_OP(atan, float, atanf);
80-
UNARY_OP(cos, double, cos);
81-
UNARY_OP(cos, float, cosf);
82-
UNARY_OP(sin, double, sin);
83-
UNARY_OP(sin, float, sinf);
84-
UNARY_OP(tan, double, tan);
85-
UNARY_OP(tan, float, tanf);
72+
UNARY_OP(sqrt, double, sqrt); // NOWARN
73+
UNARY_OP(sqrt, float, sqrtf); // NOWARN
74+
UNARY_OP(acos, double, acos); // NOWARN
75+
UNARY_OP(acos, float, acosf); // NOWARN
76+
UNARY_OP(asin, double, asin); // NOWARN
77+
UNARY_OP(asin, float, asinf); // NOWARN
78+
UNARY_OP(atan, double, atan); // NOWARN
79+
UNARY_OP(atan, float, atanf); // NOWARN
80+
UNARY_OP(cos, double, cos); // NOWARN
81+
UNARY_OP(cos, float, cosf); // NOWARN
82+
UNARY_OP(sin, double, sin); // NOWARN
83+
UNARY_OP(sin, float, sinf); // NOWARN
84+
UNARY_OP(tan, double, tan); // NOWARN
85+
UNARY_OP(tan, float, tanf); // NOWARN
8686

8787
#define BINARY_OP(name, type, op) \
8888
CAMLprim value name##_##type(value mode, value x, value y) \
@@ -99,14 +99,14 @@ UNARY_OP(tan, float, tanf);
9999
/* No need to use CAMLreturn because we don't use CAMLparam. */ \
100100
}
101101

102-
BINARY_OP(add, double, +);
103-
BINARY_OP(add, float, +);
104-
BINARY_OP(sub, double, -);
105-
BINARY_OP(sub, float, -);
106-
BINARY_OP(mul, double, *);
107-
BINARY_OP(mul, float, *);
108-
BINARY_OP(div, double, /);
109-
BINARY_OP(div, float, /);
102+
BINARY_OP(add, double, +); // NOWARN
103+
BINARY_OP(add, float, +); // NOWARN
104+
BINARY_OP(sub, double, -); // NOWARN
105+
BINARY_OP(sub, float, -); // NOWARN
106+
BINARY_OP(mul, double, *); // NOWARN
107+
BINARY_OP(mul, float, *); // NOWARN
108+
BINARY_OP(div, double, /); // NOWARN
109+
BINARY_OP(div, float, /); // NOWARN
110110

111111
CAMLprim value atof_double(value mode, value str)
112112
{
@@ -115,7 +115,7 @@ CAMLprim value atof_double(value mode, value str)
115115
// We have already read their values by then.
116116
const char *s = String_val(str);
117117
volatile double r;
118-
int old_roundingmode = fegetround();
118+
int old_roundingmode = fegetround(); // NOWARN
119119
change_round_mode(Int_val(mode));
120120
r = atof(s);
121121
fesetround(old_roundingmode);

‎tests/regression/90-ocaml/03-demimarie.c‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,24 @@
22

33
// OCaml code fixed by Demi Marie Obenour in https://github.com/ocaml/ocaml/pull/13370, before and after the fix.
44

5+
#include <caml/mlvalues.h>
6+
#include <caml/alloc.h>
7+
58
/* Minimal macros to mimic expected behaviour */
69
#define Wsizeof(ty) ((sizeof(ty) + sizeof(value) - 1) / sizeof(value))
710
#define LXM_val(v) ((struct LXM_state *) Data_abstract_val(v))
811

912
#define CAMLparam0() __goblint_caml_param0()
1013
#define CAMLparam1(x) __goblint_caml_param1(&x)
14+
#define CAMLlocal1(x) __goblint_caml_param1(&x) // The local and param functions behave the same for our purposes, registering variables.
15+
#define CAMLlocal3(x, y, z) __goblint_caml_param3(&x, &y, &z)
1116
#define CAMLreturn(x) return (x) // From AI - CAMLreturn needs some variable named caml__frame, which is not available in our mock CAMLparam1, so we mock the return as well.
1217

1318

1419
CAMLprim value caml_gc_counters(value v)
1520
{
16-
CAMLparam0 (); /* v is ignored */
17-
CAMLlocal1 (res);
21+
CAMLparam0(); /* v is ignored */
22+
CAMLlocal1(res);
1823

1924
/* get a copy of these before allocating anything... */
2025
double minwords = caml_gc_minor_words_unboxed();
@@ -23,16 +28,16 @@ CAMLprim value caml_gc_counters(value v)
2328
(double) Caml_state->allocated_words;
2429

2530
res = caml_alloc_3(0,
26-
caml_copy_double (minwords),
27-
caml_copy_double (prowords),
28-
caml_copy_double (majwords)); // WARN
29-
CAMLreturn (res);
31+
caml_copy_double(minwords),
32+
caml_copy_double(prowords),
33+
caml_copy_double(majwords)); // WARN
34+
CAMLreturn(res);
3035
}
3136

3237
CAMLprim value caml_gc_counters_correct(value v)
3338
{
34-
CAMLparam0 (); /* v is ignored */
35-
CAMLlocal3 (minwords_, prowords_, majwords_);
39+
CAMLparam0(); /* v is ignored */
40+
CAMLlocal3(minwords_, prowords_, majwords_);
3641

3742
/* get a copy of these before allocating anything... */
3843
double minwords = caml_gc_minor_words_unboxed();

0 commit comments

Comments
 (0)