Skip to content
Snippets Groups Projects
Commit 1a3b13c0 authored by Forget Julien's avatar Forget Julien
Browse files

New loops syntax (e.g. l:42).

parent 7d0598d5
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 122 additions and 92 deletions
simplify/abstract_wcet.ml
+ 3
− 13
View file @ 1a3b13c0
......@@ -151,21 +151,11 @@ let pow loops (h_body,w_body) (h_exit,w_exit) l it =
open Format
let pp_param out_f p =
fprintf out_f "p:%s" p
let pp_loop out_f l =
match l with
| LNamed n ->
fprintf out_f "%s" n
| LTop ->
pp_print_text out_f "__top"
let pp_annot out_f (loop, it) =
fprintf out_f "(%a,%d)" pp_loop loop it
fprintf out_f "(%a,%d)" pp_loop_id loop it
let pp out_f (loop, (wl,last)) =
fprintf out_f "(%a;{%a,%d})" pp_loop loop
fprintf out_f "(%a;{%a,%d})" pp_loop_id loop
(pp_print_list
~pp_sep:(fun out_f () -> pp_print_text out_f ",")
(fun out_f w -> fprintf out_f "%d" w))
......
simplify/lexer.mll
+ 1
− 0
View file @ 1a3b13c0
......@@ -53,6 +53,7 @@ rule token = parse
| ',' {COMMA}
| ';' {SCOL}
| "p:" {PARAM}
| "l:" {LOOP_ID}
| "_C" {INC}
| ['0'-'9']+
{INT (int_of_string (Lexing.lexeme lexbuf)) }
......
simplify/loops.ml
+ 21
− 10
View file @ 1a3b13c0
......@@ -20,6 +20,7 @@
*---------------------------------------------------------------------------- *)
open Utils
open Symbol
type loop_id = LNamed of string | LTop
......@@ -30,11 +31,18 @@ type hierarchy = ((string * string), unit) Hashtbl.t
type bounds = (string, symb_int) Hashtbl.t
let lname_from_lid lid =
match lid with
| LNamed n -> n
| LTop -> internal_error "bounds_from_list" "cannot set an iteration bound on top"
let new_hierarchy () : hierarchy = Hashtbl.create 42
(* Loop [inner] is included into all loops of list [outer]. *)
let add_inclusions hier inner outers =
List.iter (fun outer -> Hashtbl.add hier (inner,outer) ()) outers
List.iter (fun outer ->
Hashtbl.add hier (lname_from_lid inner,lname_from_lid outer) ())
outers
(* Returns true if [l1] is immediately contained in [l2]. *)
let imm_contained hier l1 l2 =
......@@ -63,21 +71,24 @@ let add_bound 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
let lname = lname_from_lid lid in
Hashtbl.add bounds lname bound) l;
bounds
open Format
let pp_loop out_f l =
pp_print_text out_f l
let pp_loop_id out_f l =
match l with
| LNamed n ->
fprintf out_f "l:%s" n
| LTop ->
pp_print_text out_f "__top"
let pp_hier out_f hier =
fprintf out_f "@[<hov 2>loops:@ ";
Hashtbl.iter
(fun (n1,n2) _ -> fprintf out_f "@[<hov 2>%a _C %a;@ @]" pp_loop n1 pp_loop n2)
(fun (n1,n2) _ ->
fprintf out_f "@[<hov 2>%a _C %a;@ @]"
pp_loop_id (LNamed n1) pp_loop_id (LNamed n2))
hier;
fprintf out_f "endl@]"
simplify/parser.mly
+ 7
− 6
View file @ 1a3b13c0
......@@ -21,6 +21,7 @@
%{
open Utils
open Symbol
open Loops
open Abstract_wcet
open Wcet_formula
......@@ -32,7 +33,7 @@
%token DOT
%token UNION PLUS
%token CIRC
%token LPAR RPAR LCURLBRACKET RCURLBRACKET COMMA SCOL TOP INC PARAM
%token LPAR RPAR LCURLBRACKET RCURLBRACKET COMMA SCOL TOP INC PARAM LOOP_ID
%token LOOPS ENDLH
%token EOF
......@@ -76,11 +77,11 @@ loop_inc_list:
}
loop_inc:
IDENT INC ident_list SCOL { ($1, $3)}
loop_id INC loop_id_list SCOL { ($1, $3)}
ident_list:
IDENT {[$1]}
| ident_list IDENT {$2::$1}
loop_id_list:
loop_id {[$1]}
| loop_id_list loop_id {$2::$1}
// Restrict to binary arity operators.
// Can't think of a simple solution to directly parse a full list of operands.
......@@ -126,7 +127,7 @@ INT {[$1]}
loop_id:
TOP {LTop}
| IDENT { LNamed $1}
| LOOP_ID INT { LNamed (string_of_int $2)}
annot:
LPAR loop_id COMMA INT RPAR { ($2, $4) }
......
simplify/simplify.ml
+ 1
− 0
View file @ 1a3b13c0
......@@ -20,6 +20,7 @@
*---------------------------------------------------------------------------- *)
open Utils
open Symbol
open Loops
open Abstract_wcet
open Wcet_formula
......
simplify/symbol.ml 0 → 100644
+ 37
− 0
View file @ 1a3b13c0
(* ----------------------------------------------------------------------------
* 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 param = string
(** Symbolic integer is either a constant or a symbol *)
type symb_int = SInt of int | SParam of param
open Format
let pp_param out_f p =
fprintf out_f "p:%s" p
let pp_symb_int out_f sint =
match sint with
| SInt i ->
fprintf out_f "%d" i
| SParam p ->
pp_param out_f p
simplify/test/annot.expect
+ 2
− 2
View file @ 1a3b13c0
(l1;{5,3,0}) loops: endl
((l1;{5,3,0}) + p:1) loops: endl
(l:1;{5,3,0}) loops: endl
((l:1;{5,3,0}) + p:1) loops: endl
simplify/test/annot.pwf
+ 2
− 2
View file @ 1a3b13c0
(l1;{5,3,2})|(l1,2) loops: endl
(l1;{5,3,2})|(l1,2) + p:1 loops: endl
(l:1;{5,3,2})|(l:1,2) loops: endl
(l:1;{5,3,2})|(l:1,2) + p:1 loops: endl
simplify/test/distributivity.expect
+ 6
− 6
View file @ 1a3b13c0
6.(p:1) loops: endl
(l1;{30,18,12}) loops: endl
6.(((l1;{5,3,2}) + p:1)) loops: endl
(l:1;{30,18,12}) loops: endl
6.(((l:1;{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
4.(((l:1;{5,3,2}) U p:1)) loops: endl
(((l:1;{5,4,3,2})) + p:1) loops: endl
((l:1;{5,4,3,2}) U p:1 U p:2) loops: endl
2.(((l:1;{5,5,3,3,2}) U p:1)) loops: endl
simplify/test/distributivity.pwf
+ 6
− 6
View file @ 1a3b13c0
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.2.(l:1;{5,3,2}) loops: endl
3.2.((l:1;{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
3.((p:1 U (l:1;{5,3,2}))) + (l:1;{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
((l:1;{5,3,2}) + p:1) U ((l:1;{4,1}) + p:1) loops: endl
p:2 U p:1 U (l:1;{4,1}) U (l:1;{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
(l:1;{5,3,2}) U p:1 U (l:1;{5,3,2}) + (l:1;{5,3,2}) U p:1 U (l:1;{5,3,2}) loops: endl
\ No newline at end of file
simplify/test/loops.expect
+ 7
− 7
View file @ 1a3b13c0
(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
(l2;{28,17}) loops: l2 _C l1; endl
(l1;{28,17}) loops: endl
(l1;{28,25}) loops: l1 _C l2; endl
(l:2;{10,6,4}) loops: l:2 _C l:1; endl
(l:1;{5,5,3,3,2}) loops: l:1 _C l:2; endl
(l:1;{5,3,0}) loops: l:1 _C l:2; endl
(l:1;{28,25}) loops: endl
(l:2;{28,17}) loops: l:2 _C l:1; endl
(l:1;{28,17}) loops: endl
(l:1;{28,25}) loops: l:1 _C l:2; endl
simplify/test/loops.pwf
+ 7
− 7
View file @ 1a3b13c0
(l1;{5,3,2}) + (l2;{5,3,2}) loops: l2 _C l1; endl
(l1;{5,3,2}) U (l2;{5,3,2}) loops: l1 _C l2; endl
(l1;{5,3,2})|(l2,2) loops: l1 _C l2; endl
(l:1;{5,3,2}) + (l:2;{5,3,2}) loops: l:2 _C l:1; endl
(l:1;{5,3,2}) U (l:2;{5,3,2}) loops: l:1 _C l:2; endl
(l:1;{5,3,2})|(l:2,2) loops: l:1 _C l:2; endl
((l1;{5,3,2}) + (l1;{5,3,2}), (l1;{4,1}), l1)^4 loops: endl
((l1;{5,3,2}) + (l2;{5,3,2}), (l1;{4,1}), l1)^4 loops: l2 _C l1; endl
((l1;{5,3,2}) + (l1;{5,3,2}), (l1;{4,1}), l2)^4 loops: endl
((l1;{5,3,2}) + (l2;{5,3,2}), (l1;{4,1}), l1)^4 loops: l1 _C l2; endl
((l:1;{5,3,2}) + (l:1;{5,3,2}), (l:1;{4,1}), l:1)^4 loops: endl
((l:1;{5,3,2}) + (l:2;{5,3,2}), (l:1;{4,1}), l:1)^4 loops: l:2 _C l:1; endl
((l:1;{5,3,2}) + (l:1;{5,3,2}), (l:1;{4,1}), l:2)^4 loops: endl
((l:1;{5,3,2}) + (l:2;{5,3,2}), (l:1;{4,1}), l:1)^4 loops: l:1 _C l:2; endl
simplify/test/plus_union.expect
+ 6
− 6
View file @ 1a3b13c0
(l1;{15,9,6}) 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:1) loops: endl
((l1;{20,12,8}) + 2.(p:1)) loops: endl
(l1;{10,10,10,6,6,6,4}) loops: endl
(l:1;{15,9,6}) loops: endl
((l:1;{10,6,4}) + p:1) loops: endl
(l:1;{5,5,5,3,3,3,2}) loops: endl
((l:1;{5,5,3,3,2}) U p:1) loops: endl
((l:1;{20,12,8}) + 2.(p:1)) loops: endl
(l:1;{10,10,10,6,6,6,4}) loops: endl
simplify/test/plus_union.pwf
+ 6
− 6
View file @ 1a3b13c0
(l1;{5,3,2}) + (l1;{5,3,2}) + (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: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
(l:1;{5,3,2}) + (l:1;{5,3,2}) + (l:1;{5,3,2}) loops: endl
(l:1;{5,3,2}) + p:1 + (l:1;{5,3,2}) loops: endl
(l:1;{5,3,2}) U (l:1;{5,3,2}) U (l:1;{5,3,2}) loops: endl
(l:1;{5,3,2}) U p:1 U (l:1;{5,3,2}) loops: endl
(l:1;{5,3,2}) + p:1 + (l:1;{5,3,2}) + (l:1;{5,3,2}) + p:1 + (l:1;{5,3,2}) loops: endl
(l:1;{5,3,2}) U (l:1;{5,3,2}) U (l:1;{5,3,2}) + (l:1;{5,3,2}) U (l:1;{5,3,2}) U (l:1;{5,3,2}) loops: endl
simplify/test/power.expect
+ 4
− 4
View file @ 1a3b13c0
(l1;{16,13}) loops: endl
(l1;{16,9}) 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
(l:1;{16,13}) loops: endl
(l:1;{16,9}) loops: endl
((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1 loops: endl
2.(((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1) loops: endl
simplify/test/power.pwf
+ 4
− 4
View file @ 1a3b13c0
((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)^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
((l:1;{5,3,2}), (l:1;{4,1}), l:1)^4 loops: endl
((l:1;{5,3,2}), (l:1;{4,1}), l:2)^4 loops: endl
((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1 loops: endl
((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1+((l:1;{5,3,2}), (l:1;{4,1}), l:2)^p:1 loops: endl
\ No newline at end of file
simplify/utils.ml
+ 0
− 5
View file @ 1a3b13c0
......@@ -19,10 +19,5 @@
* USA
*---------------------------------------------------------------------------- *)
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
+ 2
− 8
View file @ 1a3b13c0
......@@ -20,6 +20,7 @@
*---------------------------------------------------------------------------- *)
open Utils
open Symbol
open Loops
open Abstract_wcet
......@@ -51,13 +52,6 @@ let int_of_symb sint =
open Format
let pp_symb_int out_f sint =
match sint with
| SInt i ->
fprintf out_f "%d" i
| SParam p ->
pp_param out_f p
let rec pp out_f f =
match f with
| FConst w ->
......@@ -79,7 +73,7 @@ let rec pp out_f f =
pp out_f
) fl
| FPower (f1, f2, l, it) ->
fprintf out_f "@[<hov 2>(%a, %a, %a)^%a@]" pp f1 pp f2 pp_loop l pp_symb_int it
fprintf out_f "@[<hov 2>(%a, %a, %a)^%a@]" pp f1 pp f2 pp_loop_id l pp_symb_int it
| FAnnot (f, a) ->
fprintf out_f "@[<hov 2>%a|%a@]" pp f pp_annot a
| FProduct (k, f) ->
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment