Merge branch 'master' of gitlab.cristal.univ-lille.fr:otawa-plugins/cftreeextractor

simplify/abstract_wcet.ml

@@ -69,7 +69,7 @@ let rec sum_mwcet w1 w2  =
 
 (** Returns the sum of two abstract wcets. *)    
 let sum loops (l1,w1) (l2,w2) =
-  (Loops.max loops l1 l2, sum_mwcet w1 w2)
+  (Loops.glb loops l1 l2, sum_mwcet w1 w2)
 
 (* Union on multi_wcet. *)  
 let rec union_mwcet w1 w2 =
@@ -92,7 +92,7 @@ let rec union_mwcet w1 w2 =
 
 (** Returns the union of two abstract wcets. *)     
 let union loops (l1,w1) (l2,w2) =
-  (Loops.max loops l1 l2, union_mwcet w1 w2)
+  (Loops.glb loops l1 l2, union_mwcet w1 w2)
 
 (* Multiply [(wl,last)] by [k]. *)  
 let prod_mwcet k (wl,last) =
@@ -111,7 +111,7 @@ let rec keep_first n w =
 
 (** Computes the application of annotation [(l',it)] on abstract wcet [(l, w)] *)
 let annot loops (l, w) (l',it) =
-  (Loops.max loops l l', keep_first it w)
+  (Loops.glb loops l l', keep_first it w)
 
 (* Several auxilliary operations on loops. *)  
 
@@ -145,14 +145,14 @@ let pow loops (h_body,w_body) (h_exit,w_exit) l it =
   if h_body = l then
     (h_exit,sum_mwcet (wl_sum_k_first it w_body) w_exit)
   else
-    (Loops.max loops h_body h_exit, sum_mwcet (pack it w_body) w_exit)
+    (Loops.glb loops h_body h_exit, sum_mwcet (pack it w_body) w_exit)
 
 (* Pretty printing *)
   
 open Format
    
 let pp_param out_f p =
-  pp_print_text out_f p
+  fprintf out_f "p:%s" p
    
 let pp_loop out_f l =
   match l with

simplify/lexer.mll

@@ -52,6 +52,7 @@ rule token = parse
 | '}' {RCURLBRACKET}
 | ',' {COMMA}
 | ';' {SCOL}
+| "p:" {PARAM}
 | "_C" {INC}
 | ['0'-'9']+
     {INT (int_of_string (Lexing.lexeme lexbuf)) }

simplify/loops.ml

@@ -42,11 +42,14 @@ let imm_contained hier l1 l2 =
   | LNamed n1, LNamed n2 ->
      Hashtbl.mem hier (n1,n2)
 
-let max hier l1 l2 =
-  if (imm_contained hier l1 l2) then
+let min hier l1 l2 =
+  if (imm_contained hier l2 l1) then
     l2
   else l1
     
+let glb hier l1 l2 =
+  min hier l1 l2
+
 open Format
 
 let pp_loop out_f l =

simplify/main.ml

@@ -4,6 +4,8 @@ open Simplify
 
 let usage = "Usage: simplify <source-file>"
 
+let extension = ".pwf"
+          
 (* Simplify a list of formulas and pretty-print the results. *)          
 let simplify_prog formulas =
   List.iter
@@ -17,6 +19,8 @@ let simplify_prog formulas =
 
 (* Process file named [source_name]. Results is printed on standard output. *)  
 let anonymous source_name =
+  if Filename.check_suffix source_name extension then
+    begin
       Location.input_name := source_name;
       let lexbuf = Lexing.from_channel (open_in source_name) in
       Location.init lexbuf source_name;
@@ -28,6 +32,9 @@ let anonymous source_name =
                                   raise exc
       in
       simplify_prog prog
+    end
+  else
+    raise (Arg.Bad ("Can only process *.pwf files"))
 
 (* Do the job. *)  
 let _ =

simplify/parser.mly

@@ -31,7 +31,7 @@
 %token DOT
 %token UNION PLUS
 %token CIRC
-%token LPAR RPAR LCURLBRACKET RCURLBRACKET COMMA SCOL TOP INC
+%token LPAR RPAR LCURLBRACKET RCURLBRACKET COMMA SCOL TOP INC PARAM
 %token LOOPS ENDLH
                                                     
 %token EOF
@@ -80,7 +80,7 @@ ident_list:
       
 formula:
     const { FConst $1 }
-  | IDENT { FParam $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] }
@@ -111,4 +111,7 @@ LPAR loop_id COMMA INT RPAR { ($2, $4) }
 
 sint:
 INT {SInt $1}
-| IDENT { SParam $1}
+| param { SParam $1}
+
+param:
+  PARAM INT { string_of_int $2 }

simplify/test.sh

 TOOL=./simplify
+EXTENSION=pwf
 
 for f in `ls test`; do
-    BNAME=`basename $f .in`
+    BNAME=`basename $f .$EXTENSION`
     if [ $BNAME != $f ]; then
         IN=test/$f
         OUT=test/$BNAME".out"
         EXPECT=test/$BNAME".expect"
 
+        echo Processing $IN
         $TOOL $IN > $OUT
         diff $OUT $EXPECT
-        if [ $? -eq 1 ]; then
-            echo Diff non-empty for \"$IN\"
-        fi
     fi
 done
 
-echo "All done"
+echo "Done"

simplify/test/annot.expect

 (l1;{5,3,0}) loops: endl
-((l1;{5,3,0}) + p) loops: endl
+((l1;{5,3,0}) + p:1) loops: endl

simplify/test/annot.in → simplify/test/annot.pwf

 (l1;{5,3,2})|(l1,2) loops: endl
-(l1;{5,3,2})|(l1,2) + p loops: endl
+(l1;{5,3,2})|(l1,2) + p:1 loops: endl

simplify/test/distributivity.expect

-6.(p) loops: endl
+6.(p:1) loops: endl
 (l1;{30,18,12}) loops: endl
-6.(((l1;{5,3,2}) + p)) loops: endl
-4.(p) loops: endl
-4.(((l1;{5,3,2}) U p)) loops: endl
-(((l1;{5,4,3,2})) + p) loops: endl
-((l1;{5,4,3,2}) U p U p2) loops: endl
-2.(((l1;{5,5,3,3,2}) U p)) loops: endl
+6.(((l1;{5,3,2}) + p:1)) loops: endl
+4.(p:1) loops: endl
+4.(((l1;{5,3,2}) U p:1)) loops: endl
+(((l1;{5,4,3,2})) + p:1) loops: endl
+((l1;{5,4,3,2}) U p:1 U p:2) loops: endl
+2.(((l1;{5,5,3,3,2}) U p:1)) loops: endl

simplify/test/distributivity.in

-3.2.(p) loops: endl
-3.2.(l1;{5,3,2}) loops: endl
-3.2.((l1;{5,3,2}) + p) loops: endl
-3.(p) + p loops: endl
-3.((p U (l1;{5,3,2}))) + (l1;{5,3,2}) U p loops: endl
-
-((l1;{5,3,2}) + p) U ((l1;{4,1}) + p) loops: endl
-p2 U p U (l1;{4,1}) U (l1;{5,3,2}) loops: endl
-
-(l1;{5,3,2}) U p U (l1;{5,3,2}) + (l1;{5,3,2}) U p U (l1;{5,3,2}) loops: endl
\ No newline at end of file

simplify/test/distributivity.pwf

+3.2.(p:1) loops: endl
+3.2.(l1;{5,3,2}) loops: endl
+3.2.((l1;{5,3,2}) + p:1) loops: endl
+3.(p:1) + p:1 loops: endl
+3.((p:1 U (l1;{5,3,2}))) + (l1;{5,3,2}) U p:1 loops: endl
+
+((l1;{5,3,2}) + p:1) U ((l1;{4,1}) + p:1) loops: endl
+p:2 U p:1 U (l1;{4,1}) U (l1;{5,3,2}) loops: endl
+
+(l1;{5,3,2}) U p:1 U (l1;{5,3,2}) + (l1;{5,3,2}) U p:1 U (l1;{5,3,2}) loops: endl
\ No newline at end of file

simplify/test/loops.expect

-(l1;{10,6,4}) loops: l2 _C l1; endl
-(l2;{5,5,3,3,2}) loops: l1 _C l2; endl
-(l2;{5,3,0}) loops: l1 _C l2; endl
+(l2;{10,6,4}) loops: l2 _C l1; endl
+(l1;{5,5,3,3,2}) loops: l1 _C l2; endl
+(l1;{5,3,0}) loops: l1 _C l2; endl
 (l1;{28,25}) loops: endl
-(l1;{28,25}) loops: l2 _C l1; endl
+(l2;{28,17}) loops: l2 _C l1; endl
 (l1;{28,17}) loops: endl
-(l2;{28,17}) loops: l1 _C l2; endl
+(l1;{28,25}) loops: l1 _C l2; endl

simplify/test/plus_union.expect

 (l1;{15,9,6}) loops: endl
-((l1;{10,6,4}) + p) loops: endl
+((l1;{10,6,4}) + p:1) loops: endl
 (l1;{5,5,5,3,3,3,2}) loops: endl
-((l1;{5,5,3,3,2}) U p) loops: endl
-((l1;{20,12,8}) + 2.(p)) loops: endl
+((l1;{5,5,3,3,2}) U p:1) loops: endl
+((l1;{20,12,8}) + 2.(p:1)) loops: endl
 (l1;{10,10,10,6,6,6,4}) loops: endl

simplify/test/plus_union.in → simplify/test/plus_union.pwf

 (l1;{5,3,2}) + (l1;{5,3,2}) + (l1;{5,3,2}) loops: endl
-(l1;{5,3,2}) + p + (l1;{5,3,2}) loops: endl
+(l1;{5,3,2}) + p:1 + (l1;{5,3,2}) loops: endl
 (l1;{5,3,2}) U (l1;{5,3,2}) U (l1;{5,3,2}) loops: endl
-(l1;{5,3,2}) U p U (l1;{5,3,2}) loops: endl
-(l1;{5,3,2}) + p + (l1;{5,3,2}) + (l1;{5,3,2}) + p + (l1;{5,3,2}) loops: endl
+(l1;{5,3,2}) U p:1 U (l1;{5,3,2}) loops: endl
+(l1;{5,3,2}) + p:1 + (l1;{5,3,2}) + (l1;{5,3,2}) + p:1 + (l1;{5,3,2}) loops: endl
 (l1;{5,3,2}) U (l1;{5,3,2}) U (l1;{5,3,2}) + (l1;{5,3,2}) U (l1;{5,3,2}) U (l1;{5,3,2}) loops: endl

simplify/test/power.expect

 (l1;{16,13}) loops: endl
 (l1;{16,9}) loops: endl
-((l1;{5,3,2}), (l1;{4,1}), l2)^n loops: endl
-2.(((l1;{5,3,2}), (l1;{4,1}), l2)^n) loops: endl
+((l1;{5,3,2}), (l1;{4,1}), l2)^p:1 loops: endl
+2.(((l1;{5,3,2}), (l1;{4,1}), l2)^p:1) loops: endl

simplify/test/power.in → simplify/test/power.pwf

 ((l1;{5,3,2}), (l1;{4,1}), l1)^4 loops: endl
 ((l1;{5,3,2}), (l1;{4,1}), l2)^4 loops: endl
-((l1;{5,3,2}), (l1;{4,1}), l2)^n loops: endl
-((l1;{5,3,2}), (l1;{4,1}), l2)^n+((l1;{5,3,2}), (l1;{4,1}), l2)^n loops: endl
\ No newline at end of file
+((l1;{5,3,2}), (l1;{4,1}), l2)^p:1 loops: endl
+((l1;{5,3,2}), (l1;{4,1}), l2)^p:1+((l1;{5,3,2}), (l1;{4,1}), l2)^p:1 loops: endl
\ No newline at end of file