Skip to content

Commit 964f974

Browse files
sim642sim642
committed
Merge branch 'master' into interactive
2 parents 28c3089 + f8ad4ab commit 964f974

File tree

16 files changed

+155
-61
lines changed

16 files changed

+155
-61
lines changed

‎.github/workflows/semgrep.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ jobs:
2727
SEMGREP_AGENT_DEBUG: 1 # https://github.com/returntocorp/semgrep-action/issues/429
2828

2929
- name: Upload SARIF file to GitHub Advanced Security Dashboard
30-
uses: github/codeql-action/upload-sarif@v1
30+
uses: github/codeql-action/upload-sarif@v2
3131
with:
3232
sarif_file: semgrep.sarif
3333
if: always()

‎src/analyses/accessAnalysis.ml‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,12 @@ struct
6666
()
6767

6868
let side_access ctx ty lv_opt (conf, w, loc, e, a) =
69+
let ty =
70+
if Option.is_some lv_opt then
71+
`Type Cil.voidType (* avoid unsound type split for alloc variables *)
72+
else
73+
ty
74+
in
6975
if !GU.should_warn then
7076
ctx.sideg (V.access (lv_opt, ty)) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
7177
side_vars ctx lv_opt ty
@@ -199,8 +205,16 @@ struct
199205
| Some fnc -> (fnc act arglist)
200206
| _ -> arglist
201207
in
202-
List.iter (access_one_top ctx false true) (arg_acc `Read);
203-
List.iter (access_one_top ctx true true ) (arg_acc `Write);
208+
(* TODO: per-argument reach *)
209+
let reach =
210+
match f.vname with
211+
| "memset" | "__builtin_memset" | "__builtin___memset_chk" -> false
212+
| "bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk" -> false
213+
| "__builtin_object_size" -> false
214+
| _ -> true
215+
in
216+
List.iter (access_one_top ctx false reach) (arg_acc `Read);
217+
List.iter (access_one_top ctx true reach) (arg_acc `Write);
204218
(match lv with
205219
| Some x -> access_one_top ctx true false (AddrOf x)
206220
| None -> ());

‎src/analyses/base.ml‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -815,6 +815,8 @@ struct
815815
match ofs with
816816
| NoOffset -> `NoOffset
817817
| Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs)
818+
| Index (CastE (TInt(IInt,[]), Const (CStr ("unknown",No_encoding))), ofs) -> (* special offset added by convertToQueryLval *)
819+
`Index (IdxDom.top (), convert_offset a gs st ofs)
818820
| Index (exp, ofs) ->
819821
let exp_rv = eval_rv a gs st exp in
820822
match exp_rv with
@@ -2120,6 +2122,40 @@ struct
21202122
let st: store = ctx.local in
21212123
let gs = ctx.global in
21222124
match LF.classify f.vname args with
2125+
| `Unknown (("memset" | "__builtin_memset" | "__builtin___memset_chk") as name) ->
2126+
begin match name, args with
2127+
| "__builtin___memset_chk", [dest; ch; count; _ (* dest_size *)]
2128+
| ("memset" | "__builtin_memset"), [dest; ch; count] ->
2129+
(* TODO: check count *)
2130+
let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in
2131+
let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in
2132+
let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in
2133+
(* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2134+
let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
2135+
let value =
2136+
match eval_ch with
2137+
| `Int i when ID.to_int i = Some Z.zero ->
2138+
VD.zero_init_value dest_typ
2139+
| _ ->
2140+
VD.top_value dest_typ
2141+
in
2142+
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
2143+
| _, _ -> failwith "strange memset arguments"
2144+
end
2145+
| `Unknown (("bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk") as name) ->
2146+
(* TODO: share something with memset special case? *)
2147+
begin match name, args with
2148+
| "__explicit_bzero_chk", [dest; count; _ (* dest_size *)]
2149+
| ("bzero" | "__builtin_bzero" | "explicit_bzero"), [dest; count] ->
2150+
(* TODO: check count *)
2151+
let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in
2152+
let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in
2153+
(* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2154+
let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
2155+
let value = VD.zero_init_value dest_typ in
2156+
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
2157+
| _, _ -> failwith "strange bzero arguments"
2158+
end
21232159
| `Unknown "F59" (* strcpy *)
21242160
| `Unknown "F60" (* strncpy *)
21252161
| `Unknown "F63" (* memcpy *)

‎src/analyses/libraryFunctions.ml‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,9 @@ let invalidate_actions = [
185185
"__builtin_ctzll", readsAll;
186186
"__builtin_clz", readsAll;
187187
"bzero", writes [1]; (*keep 1*)
188+
"__builtin_bzero", writes [1]; (*keep [1]*)
189+
"explicit_bzero", writes [1];
190+
"__explicit_bzero_chk", writes [1];
188191
"connect", readsAll; (*safe*)
189192
"fclose", readsAll; (*safe*)
190193
"fflush", writesAll; (*unsafe*)
@@ -207,9 +210,9 @@ let invalidate_actions = [
207210
"mempcpy", writes [1];(*keep [1]*)
208211
"__builtin___memcpy_chk", writes [1];
209212
"__builtin___mempcpy_chk", writes [1];
210-
"memset", writesAll;(*unsafe*)
211-
"__builtin_memset", writesAll;(*unsafe*)
212-
"__builtin___memset_chk", writesAll;
213+
"memset", writes [1];(*unsafe*)
214+
"__builtin_memset", writes [1];(*unsafe*)
215+
"__builtin___memset_chk", writes [1];
213216
"printf", readsAll;(*safe*)
214217
"__printf_chk", readsAll;(*safe*)
215218
"printk", readsAll;(*safe*)
@@ -398,7 +401,6 @@ let invalidate_actions = [
398401
"__maskrune", writesAll; (*unsafe*)
399402
"inet_addr", readsAll; (*safe*)
400403
"gethostbyname", readsAll; (*safe*)
401-
"__builtin_bzero", writes [1]; (*keep [1]*)
402404
"setsockopt", readsAll; (*safe*)
403405
"listen", readsAll; (*safe*)
404406
"getsockname", writes [1;3]; (*keep [1;3]*)

‎src/analyses/varEq.ml‎

Lines changed: 9 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,7 @@ struct
193193
let bt =
194194
match unrollTypeDeep (Cilfacade.typeOf b) with
195195
| TPtr (t,_) -> t
196+
| exception Cilfacade.TypeOfError _
196197
| _ -> voidType
197198
in (* type of thing that changed: typeof( *b ) *)
198199
let rec type_may_change_apt a =
@@ -408,40 +409,6 @@ struct
408409
in
409410
List.fold_right reachable es (Some (Queries.LS.empty ()))
410411

411-
let rec reachable_from (r:Queries.LS.t) e =
412-
if Queries.LS.is_top r then true else
413-
let rec is_prefix x1 x2 =
414-
match x1, x2 with
415-
| _, `NoOffset -> true
416-
| Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> is_prefix o1 o2
417-
| Index (_,o1), `Index (_,o2) -> is_prefix o1 o2
418-
| _ -> false
419-
in
420-
let has_reachable_prefix v1 ofs =
421-
let suitable_prefix (v2,ofs2) =
422-
CilType.Varinfo.equal v1 v2
423-
&& is_prefix ofs ofs2
424-
in
425-
Queries.LS.exists suitable_prefix r
426-
in
427-
match e with
428-
| SizeOf _
429-
| SizeOfE _
430-
| SizeOfStr _
431-
| AlignOf _
432-
| Const _
433-
| AlignOfE _
434-
| UnOp _
435-
| BinOp _ -> true
436-
| AddrOf (Var v2,ofs)
437-
| StartOf (Var v2,ofs)
438-
| Lval (Var v2,ofs) -> has_reachable_prefix v2 ofs
439-
| AddrOf (Mem e,_)
440-
| StartOf (Mem e,_)
441-
| Lval (Mem e,_)
442-
| CastE (_,e) -> reachable_from r e
443-
| Question _ -> failwith "Logical operations should be compiled away by CIL."
444-
| _ -> failwith "Unmatched pattern."
445412

446413
(* Probably ok as is. *)
447414
let body ctx f = ctx.local
@@ -488,18 +455,16 @@ struct
488455
| None -> st2
489456

490457
let remove_reachable ctx es =
491-
match reachables (Analyses.ask_of_ctx ctx) es with
458+
let ask = Analyses.ask_of_ctx ctx in
459+
match reachables ask es with
492460
| None -> D.top ()
493461
| Some rs ->
494-
let remove_reachable1 es st =
495-
let remove_reachable2 e st =
496-
if reachable_from rs e && not (isConstant e) then remove_exp (Analyses.ask_of_ctx ctx) e st else st
497-
in
498-
D.B.fold remove_reachable2 es st
499-
in
500-
(* TODO: do something like this instead to be sound? *)
501-
(* List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) *)
502-
D.fold remove_reachable1 ctx.local ctx.local
462+
(* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction":
463+
each expression in ctx.local was checked for reachability from es/rs using very conservative but also unsound reachable_from.
464+
It is unknown, why that was necessary. *)
465+
Queries.LS.fold (fun lval st ->
466+
remove ask (Lval.CilLval.to_lval lval) st
467+
) rs ctx.local
503468

504469
let unknown_fn ctx lval f args =
505470
let args =

‎src/cdomains/valueDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -304,7 +304,7 @@ struct
304304
M.tracel "casta" "same size\n";
305305
if not (typ_eq t ta) then err "Cast to different type of same size."
306306
else (M.tracel "casta" "SUCCESS!\n"; o)
307-
| 1 -> (* cast to bigger/outer type *)
307+
| c when c > 0 -> (* cast to bigger/outer type *)
308308
M.tracel "casta" "cast to bigger size\n";
309309
if d = Some false then err "Ptr-cast to type of incompatible size!" else
310310
if o = `NoOffset then err "Ptr-cast to outer type, but no offset to remove."

‎src/domains/access.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module M = Messages
1010

1111
let is_ignorable_type (t: typ): bool =
1212
match t with
13-
| TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "spinlock_t"; _ }, _) -> true
13+
| TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "spinlock_t" | "pthread_cond_t"; _ }, _) -> true
1414
| TComp ({ cname = "lock_class_key"; _ }, _) -> true
1515
| TInt (IInt, attr) when hasAttribute "mutex" attr -> true
1616
| t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *)

‎tests/regression/01-cpa/24-library_functions.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ void test_memset() {
2323
void test_bzero() {
2424
int n = 1;
2525
bzero(&n, sizeof(int));
26-
assert(n == 1); // UNKNOWN!
26+
assert(n == 0);
2727
}
2828

2929
void test_getopt() {
@@ -52,7 +52,7 @@ void test_free() {
5252
void test_memcpy() {
5353
int dest = 0;
5454
int src = 1;
55-
55+
5656
memcpy(&dest, &src, sizeof(int));
5757

5858
assert(dest == 0); // UNKNOWN!

‎tests/regression/02-base/75-memset.c‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <string.h>
2+
#include <assert.h>
3+
4+
struct s {
5+
int x;
6+
int *p;
7+
};
8+
9+
int main() {
10+
int x;
11+
memset(&x, 0, sizeof(int));
12+
assert(x == 0);
13+
memset(&x, x, sizeof(int));
14+
assert(x == 0);
15+
memset(&x, 1, sizeof(int));
16+
assert(x == 0); // UNKNOWN
17+
18+
int *p;
19+
memset(&p, 0, sizeof(int*));
20+
assert(p == NULL);
21+
22+
struct s s;
23+
memset(&s, 0, sizeof(struct s));
24+
assert(s.x == 0);
25+
assert(s.p == NULL);
26+
return 0;
27+
}

tests/regression/02-base/75-pcwd-deref-unknown-fp.c renamed to tests/regression/02-base/76-pcwd-deref-unknown-fp.c

File renamed without changes.

0 commit comments

Comments
 (0)