Added loop bounds parsing/storage.

simplify/context.ml

+(* ----------------------------------------------------------------------------
+ * Copyright (C) 2020, Université de Lille, Lille, FRANCE
+ *
+ * This file is part of CFTExtractor.
+ *
+ * CFTExtractor 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.
+ *
+ * CFTExtractor 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
+ *---------------------------------------------------------------------------- *)
+
+type t = {formula: Wcet_formula.t;
+          loop_hierarchy: Loops.hierarchy;          
+          loop_bounds: Loops.bounds}
+
+let new_ctx f h b =
+  {formula=f; loop_hierarchy=h; loop_bounds=b}

simplify/loops.ml

@@ -26,9 +26,11 @@ type loop_id = LNamed of string | LTop
 (** If [Hashtbl.mem hier (n1, n2)], then loop [n1] is 
    immediately contained in loop [n2]. *) 
 (* Could be optimized, but not sure we need to, for now. *)
-type loop_hierarchy = ((string * string), unit) Hashtbl.t
+type hierarchy = ((string * string), unit) Hashtbl.t
 
-let new_hierarchy () : loop_hierarchy = Hashtbl.create 42
+type bounds = (string, symb_int) Hashtbl.t                    
+                    
+let new_hierarchy () : hierarchy = Hashtbl.create 42
                                  
 (* Loop [inner] is included into all loops of list [outer]. *)                                      
 let add_inclusions hier inner outers =
@@ -53,6 +55,21 @@ let min hier l1 l2 =
 let glb hier l1 l2 =
   min hier l1 l2
 
+let new_bounds () : bounds = Hashtbl.create 42
+
+let add_bound bounds lname bound =
+  Hashtbl.add bounds lname bound
+
+let bounds_from_list l =
+  let bounds = new_bounds () in
+  List.iter (fun (lid,bound) ->
+      let lname = match lid with
+        | LNamed n -> n
+        | LTop -> internal_error "bounds_from_list" "cannot set an iteration bound on top"
+      in
+      Hashtbl.add bounds lname bound) l;
+  bounds
+  
 open Format
 
 let pp_loop out_f l =

simplify/main.ml

 open Abstract_wcet
 open Wcet_formula
 open Simplify
+open Context   
           
 (* Simplify a list of formulas and pretty-print the results. *)          
 let simplify_prog formulas =
   List.iter
-    (fun (f,loops) ->
-      let f' = simplify loops f in
+    (fun ctx ->
+      let f' = simplify ctx.loop_hierarchy ctx.formula in
       Format.fprintf Format.std_formatter "%a %a@."
         Wcet_formula.pp f'
-        Loops.pp_hier loops
+        Loops.pp_hier ctx.loop_hierarchy
     )
     formulas
 

simplify/parser.mly

@@ -20,6 +20,7 @@
 /* ---------------------------------------------------------------------------- */
 
 %{
+  open Utils
   open Loops
   open Abstract_wcet
   open Wcet_formula
@@ -37,7 +38,7 @@
 %token EOF
 
 %start prog
-%type <(Wcet_formula.t * Loops.loop_hierarchy) list> prog
+%type <Context.t list> prog
 
 %nonassoc COMMA CIRC SCOL
 
@@ -51,16 +52,19 @@
 %%
                               
 prog:
-  formula_loops_list EOF { List.rev $1 }
+  context_list EOF { List.rev $1 }
 
-formula_loops_list:
-  formula_loops {[$1]}
-| formula_loops_list formula_loops {$2::$1}
+context_list:
+  context {[$1]}
+| context_list context {$2::$1}
 
-formula_loops:
-  formula loops { ($1,$2) }
+context:
+formula hierarchy {
+  let f,bl = $1 in
+  Context.new_ctx f $2 (Loops.bounds_from_list bl)
+}
 
-loops:
+hierarchy:
   LOOPS loop_inc_list ENDLH {$2}
 
 loop_inc_list:
@@ -78,18 +82,36 @@ ident_list:
   IDENT {[$1]}
 | ident_list IDENT {$2::$1}
 
+// Restrict to binary arity operators.
+// Can't think of a simple solution to directly parse a full list of operands.    
 formula:
-    const { FConst $1 }
-  | param { FParam $1 }
-  // Can't think of a simple solution to directly parse a full list of operands
-  | formula PLUS formula { FPlus [$1; $3] }
-  | formula UNION formula { FUnion [$1; $3] }
+    const { (FConst $1, []) }
+  | param { (FParam $1, []) }
+  | formula PLUS formula
+    {
+      let (f1,bl1),(f2,bl2) = $1,$3 in
+      (FPlus [f1; f2], bl1@bl2)
+    }
+  | formula UNION formula
+    {
+      let (f1,bl1),(f2,bl2) = $1,$3 in
+      (FUnion [f1; f2], bl1@bl2)
+    }
   | LPAR formula COMMA formula COMMA loop_id RPAR CIRC sint
-      { FPower ($2, $4, $6, $9) }
+    {
+      let (f1,bl1),(f2,bl2) = $2,$4 in
+      (FPower (f1, f2, $6, $9), ($6,$9)::bl1@bl2)
+    }
   | formula PIPE annot
-      { FAnnot ($1, $3)}
+    {
+      let f, bl = $1 in
+      (FAnnot (f, $3), bl)
+    }
   | INT DOT formula
-      { FProduct ($1, $3)}
+    {
+      let f, bl = $3 in
+      (FProduct ($1, f), bl)
+    }
   | LPAR formula RPAR {$2}
       
 const:

simplify/utils.ml

@@ -20,6 +20,9 @@
  *---------------------------------------------------------------------------- *)
 
 type param = string
+(** Symbolic integer is either a constant or a symbol *)   
+type symb_int = SInt of int | SParam of param
+
            
 let internal_error fun_name err =
   failwith ("Internal error: "^fun_name^", "^err)

simplify/wcet_formula.ml

@@ -23,9 +23,6 @@ open Utils
 open Loops
 open Abstract_wcet
 
-(** Symbolic integer is either a constant or a symbol *)   
-type symb_int = SInt of int | SParam of param
-
 (** The abstract WCET formula type. *)                                      
 type t =
   FConst of abstract_wcet