diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml index 721feee97b2ee97b133c0bc018f24967281a0a88..61315d1ef60ed873aa92d7798ccb352767c5d530 100644 --- a/src/plugins/region/code.ml +++ b/src/plugins/region/code.ml @@ -21,6 +21,7 @@ (**************************************************************************) open Cil_types +open Cil_datatype open Memory let typeof_array_elt ty = @@ -38,7 +39,7 @@ let rec lval (m:map) (s:stmt) (lv:lval) : node = and lhost (m:map) (s:stmt) = function | Var x -> Memory.root m x - | Mem e -> ptr m s e + | Mem e -> pointer m s e and loffset (m:map) (s:stmt) (r:node) (ty:typ)= function | NoOffset -> r @@ -55,8 +56,9 @@ and loffset (m:map) (s:stmt) (r:node) (ty:typ)= function let rc = Memory.range m ~size ~offset:0 ~length:size ~data in ignore @@ Memory.merge m r rc ; loffset m s data te ofs -and ptr m s e = - match exp m s e with None -> cell m () | Some r -> r +and pointer m s e = match exp m s e with None -> cell m () | Some r -> r + +and value m s e = ignore (exp m s e) and exp (m: map) (s:stmt) (e:exp) : node option = match e.enode with @@ -76,24 +78,24 @@ and exp (m: map) (s:stmt) (e:exp) : node option = None | UnOp(_,e,_) -> - ignore (exp m s e) ; None + value m s e ; None | BinOp((PlusPI|MinusPI),p,k,_) -> - ignore (exp m s k) ; - let r = ptr m s p in + value m s k ; + let r = pointer m s p in Memory.shift m r (Exp(s,e)) ; Some r | BinOp(_,a,b,_) -> - ignore (exp m s a) ; - ignore (exp m s b) ; + value m s a ; + value m s b ; None | CastE(ty,p) -> if Cil.isPointerType ty then - Some (ptr m s p) + Some (pointer m s p) else - (ignore (exp m s e) ; None) + (value m s e ; None) | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ @@ -137,14 +139,72 @@ let instr (m:map) (s:stmt) (instr:instr) = let acs = Access.Init(s,x) in init m s acs (Var x,NoOffset) iv - | Call _ -> - assert false + | Call(lr,e,es,_) -> + value m s e ; + List.iter (value m s) es ; + Option.iter + (fun lv -> + let r = lval m s lv in + Memory.write m r (Lval(s,lv)) + ) lr ; + Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis" | Local_init(_,ConsInit _,_) -> - Options.warning ~source:(fst @@ Cil_datatype.Stmt.loc s) + Options.warning ~source:(fst @@ Stmt.loc s) "Constructor init not yet implemented" | Asm _ -> - Options.warning ~source:(fst @@ Cil_datatype.Stmt.loc s) + Options.warning ~source:(fst @@ Stmt.loc s) "Inline assembly not supported (ignored)" (* -------------------------------------------------------------------------- *) +(* --- Statements --- *) +(* -------------------------------------------------------------------------- *) + +type rmap = Memory.map Stmt.Map.t ref + +let store rmap m s = + rmap := Stmt.Map.add s (Memory.copy m) !rmap + +let rec stmt (r:rmap) (m:map) (s:stmt) = + + let annots = Annotations.code_annot s in + if annots <> [] then + Options.warning ~source:(fst @@ Stmt.loc s) + "Annotations not analyzed" ; + match s.skind with + | Instr ki -> instr m s ki ; store r m s + | Return(Some e,_) -> value m s e ; store r m s + | Goto _ | Break _ | Continue _ | Return(None,_) -> store r m s + | If(e,st,se,_) -> + value m s e ; + store r m s ; + block r m st ; + block r m se ; + | Switch(e,b,_,_) -> + value m s e ; + store r m s ; + block r m b ; + | Block b | Loop(_,b,_,_,_) -> block r m b + | UnspecifiedSequence s -> block r m @@ Cil.block_from_unspecified_sequence s + | Throw(exn,_) -> Option.iter (fun (e,_) -> value m s e) exn + | TryCatch(b,hs,_) -> + block r m b ; + List.iter (fun (c,b) -> catch r m c ; block r m b) hs ; + | TryExcept(a,(ks,e),b,_) -> + block r m a ; + List.iter (instr m s) ks ; + value m s e ; + block r m b ; + | TryFinally(a,b,_) -> + block r m a ; + block r m b ; + +and catch (r:rmap) (m:map) (c:catch_binder) = + match c with + | Catch_all -> () + | Catch_exn(_,xbs) -> List.iter (fun (_,b) -> block r m b) xbs + +and block (r:rmap) (m:map) (b:block) = + List.iter (stmt r m) b.bstmts + +(* -------------------------------------------------------------------------- *) diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli index 9016f2094c945dcafa87b2cab066910e8b41dea2..ee2e7b9aecabc7fe920b26b46e3ab0351421442b 100644 --- a/src/plugins/region/code.mli +++ b/src/plugins/region/code.mli @@ -21,9 +21,10 @@ (**************************************************************************) open Cil_types +open Cil_datatype open Memory val lval : map -> stmt -> lval -> node -val ptr : map -> stmt -> exp -> node val exp : map -> stmt -> exp -> node option val instr : map -> stmt -> instr -> unit +val stmt : map Stmt.Map.t ref -> map -> stmt -> unit