Skip to content

Commit ac8e0c4

Browse files
committed
[semantics] merge library and api functions for patron
1 parent b173273 commit ac8e0c4

File tree

2 files changed

+28
-2
lines changed

2 files changed

+28
-2
lines changed

src/semantics/apiSem.ml

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ let api_map =
9090
|> ApiMap.add "memmove"
9191
{ arg_typs = [ dst; arr_src; Size ]; ret_typ = DstArg }
9292
|> ApiMap.add "strcpy" { arg_typs = [ dst; arr_src ]; ret_typ = DstArg }
93+
|> ApiMap.add "g_strdup" { arg_typs = [ arr_src ]; ret_typ = AllocDst }
9394
|> ApiMap.add "strncpy"
9495
{ arg_typs = [ dst; arr_src; Size ]; ret_typ = DstArg }
9596
|> ApiMap.add "strxfrm"
@@ -239,6 +240,7 @@ let api_map =
239240
|> ApiMap.add "pclose" { arg_typs = [ Skip ]; ret_typ = int_v }
240241
|> ApiMap.add "_IO_getc" { arg_typs = [ Skip ]; ret_typ = tainted_v }
241242
|> ApiMap.add "getchar" { arg_typs = []; ret_typ = tainted_v }
243+
|> ApiMap.add "getc" { arg_typs = [ Skip ]; ret_typ = tainted_v }
242244
|> ApiMap.add "read" { arg_typs = [ Skip; buf; Size ]; ret_typ = SizeArg }
243245
|> ApiMap.add "fread"
244246
{ arg_typs = [ buf; Skip; Size; Skip ]; ret_typ = SizeArg }
@@ -261,6 +263,7 @@ let api_map =
261263
|> ApiMap.add "getenv" { arg_typs = [ Skip ]; ret_typ = tainted_arr }
262264
(* etc *)
263265
|> ApiMap.add "scanf" { arg_typs = [ Skip; buf_va ]; ret_typ = int_v }
266+
|> ApiMap.add "fscanf" { arg_typs = [ Skip; Skip; buf_va ]; ret_typ = int_v }
264267
|> ApiMap.add "sscanf"
265268
{ arg_typs = [ arr_src; Skip; dst_va ]; ret_typ = int_v }
266269
|> ApiMap.add "fgets" { arg_typs = [ buf; Size; Skip ]; ret_typ = BufArg }
@@ -303,3 +306,7 @@ let api_map =
303306
(* libssh *)
304307
|> ApiMap.add "_ssh_buffer_unpack"
305308
{ arg_typs = [ arr_src; Skip; Skip; dst_va ]; ret_typ = int_v }
309+
|> ApiMap.add "g_get_num_processors" { arg_typs = []; ret_typ = int_v }
310+
(* patron experiment *)
311+
|> ApiMap.add "TIFFGetField"
312+
{ arg_typs = [ Skip; Skip; buf_va ]; ret_typ = int_v }

src/semantics/taintSem.ml

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,14 +50,33 @@ let eval_bop b v1 v2 itv1 itv2 =
5050
| Cil.Lt | Cil.Gt | Cil.Le | Cil.Ge | Cil.Eq | Cil.Ne | Cil.LAnd | Cil.LOr ->
5151
Val.bot
5252

53-
let rec eval pid e itvmem mem =
53+
let rec resolve_offset pid offset itvmem mem =
54+
match offset with
55+
| Cil.NoOffset -> ()
56+
| Cil.Field (_, o) -> resolve_offset pid o itvmem mem
57+
| Cil.Index (e, o) ->
58+
let _ = eval pid e itvmem mem in
59+
resolve_offset pid o itvmem mem
60+
61+
and eval_lv pid lv itvmem mem =
62+
(match fst lv with
63+
| Cil.Mem e ->
64+
let _ = eval pid e itvmem mem in
65+
()
66+
| _ -> ());
67+
resolve_offset pid (snd lv) itvmem mem
68+
69+
and eval pid e itvmem mem =
5470
match e with
5571
| Cil.Const _ | Cil.SizeOf _ | Cil.SizeOfE _ | Cil.SizeOfStr _ | Cil.AlignOf _
5672
| Cil.AlignOfE _
5773
| Cil.UnOp (_, _, _)
5874
| Cil.AddrOf _ | Cil.AddrOfLabel _ | Cil.StartOf _ ->
5975
Val.bot
60-
| Cil.Lval l -> lookup (ItvSem.eval_lv pid l itvmem) mem
76+
| Cil.Lval l ->
77+
(* for access analysis *)
78+
eval_lv pid l itvmem mem;
79+
lookup (ItvSem.eval_lv pid l itvmem) mem
6180
| Cil.BinOp (b, e1, e2, _) ->
6281
let itv1, itv2 =
6382
( ItvSem.eval pid e1 itvmem |> ItvDom.Val.itv_of_val,

0 commit comments

Comments
 (0)