abstract_wcet.ml

(* ----------------------------------------------------------------------------
 * Copyright (C) 2020, Université de Lille, Lille, FRANCE
 *
 * This file is part of WSymb.
 *
 * WSymb is free software; 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 ; either version 2 of
 * the License, or (at your option) any later version.
 *
 * WSymb 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.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this program ; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
 * USA
 *---------------------------------------------------------------------------- *)

(** Abstract WCET definitions and operators. *)

open Utils
open Loops
   
type annot = loop_id * int

(* Might switch to symb_int later *)           
type wcet = int

(* We assume that for any [(wl, last): multi_wcet], [wl] is sorted
   decreasingly and [last] is smaller than every value in [wl]. [last]
   is implicitely repeated indefinitely. *)
type multi_wcet = wcet list * wcet

type abstract_wcet = loop_id * multi_wcet

let bot_wcet = (LTop, ([],0))

(** Returns the highest WCET of [(wl, last)] *)
let hd (wl, last) =
  if wl = [] then last (* Because last is repeated indefinitely *)
  else List.hd wl

(** Returns the given multi_wcet without its highest WCET *)  
let tl (wl, last) =
  if wl = [] then ([], last) (* Because last is repeated indefinitely *)
  else (List.tl wl,last)  

(** Inserts [w] in [(wl, last)] keeping the result sorted decreasingly. *)  
let insert w (wl, last) =
  let cmp = fun x y -> -(compare x y) in
  if w > last then
    (List.merge cmp wl [w], last) (* Keep wl sorted decreasingly. *)
  else if w = last then
    (wl, last)
  else (List.merge cmp wl [last], w) (* w is the new last, ex-last goes into wl *)

(* Sum on multi_wcet *)
let rec sum_mwcet w1 w2  =
  (* Basically, a point-by-point addition. *)
  match w1, w2 with
  | ([], last1), ([], last2) -> ([], last1+last2)
  | _,_ ->
     (* Thanks to the definition of hd, we don't need to worry about
        (w1, w2) not having the same length. *)
     insert ((hd w1) + (hd w2)) (sum_mwcet (tl w1) (tl w2))

(** Returns the sum of two abstract wcets. *)