Region.ml 21.5 KB
Newer Older
1 2 3 4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
5
(*  Copyright (C) 2007-2019                                               *)
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

23 24 25 26 27
open Cil_datatype
open Layout

module Wp = Wp_parameters

28
(* -------------------------------------------------------------------------- *)
29
(* --- Access Maps                                                        --- *)
30 31
(* -------------------------------------------------------------------------- *)

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
module Vmap = Varinfo.Map
module Smap = Datatype.String.Map
module Rmap = Qed.Intmap
module Rset = Qed.Intset
module Dmap = Qed.Listmap.Make(Offset)
module Dset = Qed.Listset.Make(Deref)
module Acs = Qed.Listset.Make(Lvalue)
module Class = Qed.Listset.Make(Datatype.String)
module Ranks = Qed.Listset.Make(Datatype.Int)

type region = {
  id : int ;
  mutable garbled : bool ;
  mutable rw : bool ;
  mutable pack : bool ;
  mutable flat : bool ;
  mutable names : Class.t ;
  mutable alias : alias ;
  mutable delta : int Dmap.t ;
  mutable deref : Dset.t ;
  mutable read : Acs.t ;
  mutable written : Acs.t ;
  mutable shifted : Acs.t ;
  mutable copiedTo : Rset.t ; (* copies to *)
  mutable pointsTo : int option ;
}

type map = {
  cache : Offset.cache ;
  queue : int Queue.t ;
  mutable rid : int ;
  mutable vars : int Vmap.t ;
  mutable return : int ; (* -1 when undefined *)
  mutable strings : (int * string) Rmap.t ; (* eid -> rid *)
  mutable index : int Smap.t ;
  mutable region : region Rmap.t ;
  mutable aliasing : int Rmap.t ;
  mutable cluster : region cluster Rmap.t ;
  mutable roots : root Rmap.t ;
  mutable froms : region from list Rmap.t ;
  mutable mranks : Ranks.t Rmap.t ; (* set of sizeof(ds) accessed by shifting *)
  mutable mdims : int list Rmap.t ; (* common dim prefix accessed from cluster *)
  mutable domain : Rset.t ; (* reachable regions via clusters *)
  mutable chunk : region chunk Rmap.t ; (* memory chunks *)
}

let create () = {
  rid = 0 ;
  return = (-1) ;
  cache = Offset.cache () ;
  vars = Vmap.empty ;
  strings = Rmap.empty ;
  index = Smap.empty ;
  region = Rmap.empty ;
  aliasing = Rmap.empty ;
  queue = Queue.create () ;
  cluster = Rmap.empty ;
  roots = Rmap.empty ;
  froms = Rmap.empty ;
  mranks = Rmap.empty ;
  mdims = Rmap.empty ;
  domain = Rset.empty ;
  chunk = Rmap.empty ;
}

let noid = 0
let is_empty map = (map.rid = 0)

let fresh map =
  let id = map.rid in
  map.rid <- succ id ;
  let region = {
    id ;
    garbled = false ;
    rw = RW.default () ;
    flat = Flat.default () ;
    pack = Pack.default () ;
    names = [] ;
    alias = NotUsed ;
    delta = Dmap.empty ;
    deref = Dset.empty ;
    read = Acs.empty ;
    written = Acs.empty ;
    shifted = Acs.empty ;
    copiedTo = Rset.empty ;
    pointsTo = None ;
  } in
  map.region <- Rmap.add id region map.region ;
  region
121

122 123 124
(* -------------------------------------------------------------------------- *)
(* --- Datatype                                                           --- *)
(* -------------------------------------------------------------------------- *)
125

126 127 128 129 130
module R =
struct
  type t = region
  let id a = a.id
  let equal a b = (a.id = b.id)
131
  let compare a b = Transitioning.Stdlib.compare a.id b.id
132 133 134
  let pp_rid fmt id = Format.fprintf fmt "R%03d" id
  let pretty fmt r = pp_rid fmt r.id
end
135

136 137
module Map = Qed.Idxmap.Make(R)
module Set = Qed.Idxset.Make(R)
138 139

(* -------------------------------------------------------------------------- *)
140
(* --- Union Find                                                         --- *)
141 142
(* -------------------------------------------------------------------------- *)

143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
let rec aliasing map i =
  try
    let j = aliasing map (Rmap.find i map.aliasing) in
    if j <> i then map.aliasing <- Rmap.add i j map.aliasing ; j
  with Not_found -> i

let linkto map i k =
  if i <> k then
    begin
      map.aliasing <- Rmap.add i k map.aliasing ;
      Queue.add i map.queue ;
    end

let region map r =
  try Rmap.find (aliasing map r) map.region
  with Not_found -> failwith "Wp.Region: Undefined Region"

let join_classes map i j =
  let k = min i j in (linkto map i k ; linkto map j k ; k)

let join_id map i j =
  let i = aliasing map i in
  let j = aliasing map j in
  if i = j then i else join_classes map i j

let join_region map ra rb =
  let i = aliasing map ra.id in
  let j = aliasing map rb.id in
  let k = join_classes map i j in
  if k = i then ra else
  if k = j then rb else
    (* defensive *) region map k
175

176 177 178
(* -------------------------------------------------------------------------- *)
(* --- Aliasing                                                           --- *)
(* -------------------------------------------------------------------------- *)
179

180 181 182 183
let alias map a b =
  let k = join_id map a.id b.id in
  let r = region map k in
  r.alias <- Aliased ; r
184

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
let do_alias map a b = ignore (alias map a b)

let add_alias map ~into:a b =
  let i = aliasing map a.id in
  let j = aliasing map b.id in
  let wa = (region map i).alias in
  let wb = (region map j).alias in
  let k = join_classes map i j in
  (* Aliasing has changed *)
  (region map k).alias <- Alias.alias wa (Alias.use wb)

let get_merged map r =
  let i = aliasing map r.id in
  if i <> r.id then Some (region map i) else None

let get_alias map r =
  let i = aliasing map r.id in
  if i <> r.id then region map i else r

let eq_alias map a b = (aliasing map a.id = aliasing map b.id)

(* -------------------------------------------------------------------------- *)
(* --- General Iterator                                                   --- *)
(* -------------------------------------------------------------------------- *)

let once mark r =
  if Rset.mem r.id !mark then false
  else ( mark := Rset.add r.id !mark ; true )

let iter map f =
  let do_once marks f r = if once marks r then f r else () in
  Rmap.iter (do_once (ref Rset.empty) f) map.region

(* -------------------------------------------------------------------------- *)
(* --- Region Accessor                                                    --- *)
(* -------------------------------------------------------------------------- *)

let id reg = reg.id
let is_garbled reg = reg.garbled
let has_pointed reg = reg.pointsTo <> None
let has_deref reg = not (Dset.is_empty reg.deref)
let has_layout reg = not (Dmap.is_empty reg.delta)
let has_offset reg d = Dmap.mem d reg.delta
let iter_offset map f reg =
  Dmap.iter (fun ofs r -> f ofs (region map r)) reg.delta

let has_copies reg = not (Rset.is_empty reg.copiedTo)
let iter_copies map f reg =
  Rset.iter (fun r -> f (region map r)) reg.copiedTo

let add_offset map reg d =
  try region map (Dmap.find d reg.delta)
  with Not_found ->
    let rd = fresh map in
    reg.delta <- Dmap.add d rd.id reg.delta ; rd

let add_pointed map reg =
  match reg.pointsTo with
  | Some k -> region map k
  | None ->
      let r = fresh map in
      reg.pointsTo <- Some r.id ; r

let get_addrof map reg =
  let addr = fresh map in
  addr.pointsTo <- Some reg.id ; addr

let get_pointed map reg =
  match reg.pointsTo with
  | None -> None
  | Some r -> Some (region map r)

let get_offset map reg d =
  try Some (region map (Dmap.find d reg.delta))
  with Not_found -> None

let get_copies map reg =
  List.map (region map) (Rset.elements reg.copiedTo)

(* -------------------------------------------------------------------------- *)
(* --- Access                                                             --- *)
(* -------------------------------------------------------------------------- *)

let acs_read rg lvalue = rg.read <- Acs.add lvalue rg.read
let acs_write rg lvalue = rg.written <- Acs.add lvalue rg.written
let acs_shift rg lvalue = rg.shifted <- Acs.add lvalue rg.shifted
let acs_deref rg deref = rg.deref <- Dset.add deref rg.deref
let acs_copy ~src ~tgt =
  if tgt.id <> src.id then src.copiedTo <- Rset.add tgt.id src.copiedTo

let iter_read f rg = Acs.iter f rg.read
let iter_write f rg = Acs.iter f rg.written
let iter_shift f rg = Acs.iter f rg.shifted
let iter_deref f rg = Dset.iter f rg.deref

let is_read rg = not (Acs.is_empty rg.read)
let is_written rg = not (Acs.is_empty rg.written)
let is_shifted rg = not (Acs.is_empty rg.shifted)
let is_aliased rg = Alias.is_aliased rg.alias

(* -------------------------------------------------------------------------- *)
(* --- Varinfo Index                                                      --- *)
(* -------------------------------------------------------------------------- *)

let rvar map x r =
  let reg = region map r in
  if reg.id <> r then map.vars <- Vmap.add x reg.id map.vars ; reg

let of_null map = fresh map (* A fresh region each time: polymorphic *)

let of_cvar map x =
  try rvar map x (Vmap.find x map.vars)
  with Not_found ->
    let reg = fresh map in
    map.vars <- Vmap.add x reg.id map.vars ; reg

let of_return map =
  if map.return < 0 then
    let reg = fresh map in
    map.return <- reg.id ; reg
  else
    region map map.return

let has_return map = 0 <= map.return

let iter_vars map f = Vmap.iter (fun x r -> f x (rvar map x r)) map.vars

(* -------------------------------------------------------------------------- *)
(* --- Field Info Index                                                   --- *)
(* -------------------------------------------------------------------------- *)

let field_offset map fd = Offset.field_offset map.cache fd

(* -------------------------------------------------------------------------- *)
(* --- String Literal Index                                               --- *)
(* -------------------------------------------------------------------------- *)

let of_cstring map ~eid ~cst =
  try region map (fst @@ Rmap.find eid map.strings)
  with Not_found ->
    let reg = fresh map in
    map.strings <- Rmap.add eid (reg.id,cst) map.strings ; reg

let iter_strings map f =
  Rmap.iter (fun (rid,cst) -> f (region map rid) cst) map.strings

(* -------------------------------------------------------------------------- *)
(* --- Region Index                                                       --- *)
(* -------------------------------------------------------------------------- *)

let rindex map a r =
  let reg = region map r in
  if reg.id <> r then map.index <- Smap.add a reg.id map.index ; reg

let of_name map a =
  try rindex map a (Smap.find a map.index)
  with Not_found ->
    let reg = fresh map in
    reg.names <- [a] ;
    map.index <- Smap.add a reg.id map.index ; reg
345

346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386
let of_class map = function
  | None -> fresh map
  | Some a -> of_name map a

let has_names reg = not (Class.is_empty reg.names)
let iter_names map f = Smap.iter (fun a r -> f a (rindex map a r)) map.index

(* -------------------------------------------------------------------------- *)
(* --- Fusion                                                             --- *)
(* -------------------------------------------------------------------------- *)

let merge_pointed map u v =
  match u,v with
  | None , w | w , None -> w
  | Some i , Some j -> Some (join_id map i j)

let merge_delta map _d a b = join_id map a b

let merge_region map ~id a b =
  {
    id ;
    garbled = a.garbled || b.garbled ;
    rw = RW.merge a.rw b.rw ;
    flat = Flat.merge a.flat b.flat ;
    pack = Pack.merge a.pack b.pack ;
    alias = Alias.merge a.alias b.alias ;
    names = Class.union a.names b.names ;
    read = Acs.union a.read b.read ;
    written = Acs.union a.written b.written ;
    shifted = Acs.union a.shifted b.shifted ;
    copiedTo = Rset.union a.copiedTo b.copiedTo ;
    pointsTo = merge_pointed map a.pointsTo b.pointsTo ;
    delta = Dmap.union (merge_delta map) a.delta b.delta ;
    deref = Dset.union a.deref b.deref ;
  }

let fusion map =
  while not (Queue.is_empty map.queue) do
    let i = Queue.pop map.queue in
    let j = aliasing map i in
    if i <> j then
387
      begin
388 389 390 391 392 393 394 395
        if not (Wp.Region_fixpoint.get ()) then
          Wp.debug "Region %a -> %a" R.pp_rid i R.pp_rid j ;
        let a = try Rmap.find i map.region with Not_found -> assert false in
        let b = try Rmap.find j map.region with Not_found -> assert false in
        assert (i = a.id) ;
        assert (j = b.id ) ;
        let c = merge_region map ~id:j a b in
        map.region <- Rmap.add j c (Rmap.remove i map.region) ;
396
      end
397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649
  done

let fusionned map = not (Queue.is_empty map.queue)
let iter_fusion map f = Queue.iter (fun i -> f i (region map i)) map.queue

(* -------------------------------------------------------------------------- *)
(* --- Garbling                                                           --- *)
(* -------------------------------------------------------------------------- *)

let rec garblify map reg =
  if not reg.garbled then
    begin
      reg.garbled <- true ;
      Dmap.iter
        (fun _delta r ->
           garblify map (region map r) ;
           ignore (join_id map reg.id r) ;
        ) reg.delta ;
      reg.delta <- Dmap.empty ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Clustering                                                         --- *)
(* -------------------------------------------------------------------------- *)

let cluster map reg =
  try Rmap.find reg.id map.cluster
  with Not_found -> Layout.Empty

module Cluster =
struct
  open Layout

  let rec from_region map reg =
    try Rmap.find reg.id map.cluster
    with Not_found ->
      if reg.garbled then Garbled else
      if not (Wp.Region_cluster.get ()) then Empty else
        begin
          map.cluster <- Rmap.add reg.id Empty map.cluster ;
          let mu ~raw ra rb =
            if raw then
              begin
                garblify map ra ;
                garblify map rb ;
              end ;
            join_region map ra rb
          in
          let cluster =
            if has_layout reg then
              Cluster.reshape ~eq:R.equal ~flat:reg.flat ~pack:reg.pack @@
              from_layout map mu reg
            else
              from_deref map mu reg
          in
          if cluster = Garbled then garblify map reg ;
          map.cluster <- Rmap.add reg.id cluster map.cluster ;
          cluster
        end

  and from_deref map mu reg =
    let pointed = lazy (add_pointed map reg) in
    List.fold_left
      (fun chunk deref ->
         Cluster.merge R.pretty mu chunk (Cluster.deref ~pointed deref)
      ) Empty reg.deref

  and from_layout map mu reg =
    Dmap.fold
      (fun offset tgt acc ->
         let layout = shift map offset (region map tgt) in
         Cluster.merge R.pretty mu (Layout layout) acc
      ) reg.delta Empty

  and shift map offset target =
    let inline = Wp.Region_inline.get () || not (is_aliased target) in
    let cluster = from_region map target in
    Cluster.shift map.cache R.pretty offset target ~inline cluster

  let compute map reg =
    begin
      if has_layout reg && has_deref reg then
        begin
          Dset.iter
            (fun deref ->
               let target = add_offset map reg (Index(snd deref,1)) in
               target.read <- Acs.union reg.read target.read ;
               target.written <- Acs.union reg.written target.written ;
               acs_deref target deref
            ) reg.deref ;
          reg.deref <- Dset.empty ;
          reg.read <- Acs.empty ;
          reg.written <- Acs.empty ;
          Queue.add reg.id map.queue ;
        end ;
      ignore (from_region map reg) ;
    end

end

(* -------------------------------------------------------------------------- *)
(* --- Froms Analysis                                                     --- *)
(* -------------------------------------------------------------------------- *)

let get_froms map reg =
  try Rmap.find reg.id map.froms
  with Not_found -> []

let add_from map ~from ~target =
  let rs = get_froms map target in
  map.froms <- Rmap.add target.id (from :: rs) map.froms

module Froms =
struct
  open Layout

  let rec forward map marks ~source ~from ~target =
    map.domain <- Rset.add source.id map.domain ;
    add_from map ~from ~target ;
    if once marks target then add_region map marks target

  and add_region map marks reg =
    begin
      add_points_to map marks ~source:reg reg.pointsTo ;
      add_cluster map marks ~source:reg (cluster map reg) ;
    end

  and add_points_to map marks ~source = function
    | None -> ()
    | Some p -> add_deref map marks ~source ~target:(region map p)

  and add_deref map marks ~source ~target =
    let from = if is_shifted target then Farray source else Fderef source in
    forward map marks ~source ~from ~target

  and add_cluster map marks ~source = function
    | Empty | Garbled | Chunk (Int _ | Float _) -> ()
    | Chunk (Pointer target) -> add_deref map marks ~source ~target
    | Layout { layout } -> List.iter (add_range map marks ~source) layout

  and add_range map marks ~source = function
    | { ofs ; reg = target ; dim = Dim(_,[]) } ->
        forward map marks ~source ~from:(Ffield(source,ofs)) ~target
    | { reg = target } ->
        forward map marks ~source ~from:(Findex source) ~target

end

(* -------------------------------------------------------------------------- *)
(* --- Roots Analysis                                                     --- *)
(* -------------------------------------------------------------------------- *)

let get_roots map reg =
  try Rmap.find reg.id map.roots
  with Not_found -> Rnone

let has_roots map reg = get_roots map reg <> Rnone

module Roots =
struct

  let rec of_region map region =
    try Rmap.find region.id map.roots
    with Not_found ->
      let froms = get_froms map region in
      let roots =
        List.fold_left
          (fun roots from ->
             Root.merge roots (Root.from ~root:(of_region map) from)
          ) Rnone froms
      in map.roots <- Rmap.add region.id roots map.roots ; roots

  let compute map reg = ignore (of_region map reg)

end

(* -------------------------------------------------------------------------- *)
(* --- Forward & Backward Propagation                                     --- *)
(* -------------------------------------------------------------------------- *)

let forward map =
  begin
    let marks = ref Rset.empty in
    map.domain <- Rset.empty ;
    Vmap.iter
      (fun x r ->
         let reg = region map r in
         let open Cil_types in
         if x.vglob || x.vformal then
           add_from map ~from:(Fvar x) ~target:(region map r) ;
         Froms.add_region map marks reg ;
      ) map.vars ;
  end

let backward map =
  begin
    Rmap.iter (Roots.compute map) map.region ;
  end

(* -------------------------------------------------------------------------- *)
(* --- Chunk Analysis                                                     --- *)
(* -------------------------------------------------------------------------- *)

let rec chunk map region =
  try Rmap.find region.id map.chunk
  with Not_found ->
    let roots = get_roots map region in
    let chunk =
      match cluster map region with
      | Empty | Garbled -> Mraw (roots,get_pointed map region)
      | Chunk v ->
          if is_read region || is_written region then
            Mmem(roots,v)
          else
            begin match v with
              | Pointer r -> Mref r
              | _ -> Mraw (roots,get_pointed map region)
            end
      | Layout { layout } ->
          let chunks = Chunk.union_map (fun { reg } -> chunks map reg) layout
          in Mcomp(chunks,layout)

    in map.chunk <- Rmap.add region.id chunk map.chunk ; chunk

and chunks map region =
  match chunk map region with
  | Mcomp(rs,_) -> rs
  | _ -> Chunk.singleton region.id

(* -------------------------------------------------------------------------- *)
(* --- Fixpoint                                                           --- *)
(* -------------------------------------------------------------------------- *)

let fixpoint map =
  begin
    let turn = ref 0 in
    let loop = ref true in
    while !loop do
      incr turn ;
      Wp.feedback ~ontty:`Transient "Region clustering (loop #%d)" !turn ;
      fusion map ;
      map.cluster <- Rmap.empty ;
      iter map (Cluster.compute map) ;
      loop := fusionned map ;
    done ;
    Wp.feedback ~ontty:`Transient "Region forward analysis" ;
    forward map ;
    Wp.feedback ~ontty:`Transient "Region backward analysis" ;
    backward map ;
    Wp.feedback ~ontty:`Transient "Region fixpoint reached" ;
  end

(* -------------------------------------------------------------------------- *)