Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (9 years ago)
Author:
tranquil
Message:
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costExpr.ml

    r1483 r1507  
    2121type cost_expr =
    2222    | Exact of int
    23     | Ternary of index * cond * cost_expr * cost_expr
     23    | Ternary of index * CondSet.t * cost_expr * cost_expr
    2424
    2525(* compute from the set [s] a the 3-uple [Some (h, s_h, s_rest)] where *)
     
    4848            let if_true = cost_mapping_ind atom (h :: ind) m s_head in
    4949            let if_false = cost_mapping_ind atom ind m s_rest in
    50             Ternary(i, condition, if_true, if_false) 
     50            Ternary(i, CondSet.singleton condition, if_true, if_false) 
    5151
    5252let indexing_sets_from_cost_mapping m =
     
    236236        let rec simplify' conds = function
    237237                | Exact k -> Exact k
    238                 | Ternary (i, cond, if_true, if_false) ->
     238                | Ternary (i, gen_cond, if_true, if_false) ->
     239                        assert (CondSet.cardinal gen_cond = 1);
     240                        let cond = CondSet.choose gen_cond in
    239241                        (* if it is the first time a condition on i is encountered, we ensure *)
    240242                        (* that conds holds a default value that will be the "true" of these *)
     
    254256                                ExtArray.set conds i (cond_and_not conds_i cond);
    255257                                let if_false' = simplify' conds if_false in
    256                                 Ternary (i, cond', if_true', if_false')
     258                                Ternary (i, CondSet.singleton cond', if_true', if_false')
    257259                        end in
    258260        let conds = ExtArray.make ~buff:4 0 (CondSet.singleton (Cgeq 0)) in
    259261        simplify' conds
    260262
     263let gen_or = CondSet.union
     264
     265let gen_and s1 s2 =
     266        let f c s = CondSet.union s (cond_and s1 c) in
     267        CondSet.fold f s2 CondSet.empty
     268       
     269let gen_and_not s1 s2 =
     270        let f c s = cond_and_not s c in
     271        CondSet.fold f s2 s1
     272       
     273let gen_not s = gen_and_not (CondSet.singleton (Cgeq 0)) s
     274
    261275let rec remove_useless_branchings = function
    262276        | Exact k -> Exact k
    263         | Ternary (i, cond, if_true, if_false) ->
    264                 let if_true' = remove_useless_branchings if_true in
    265     let if_false' = remove_useless_branchings if_false in
    266                 if if_true = if_false then if_true else
    267                 Ternary (i, cond, if_true', if_false')
     277        | Ternary (i, c1, left, right) ->
     278                let left = remove_useless_branchings left in
     279    let right = remove_useless_branchings right in
     280                match left, right with
     281                        | _, _ when left = right -> left
     282                        | Ternary(j, c2, lleft, lright), _
     283                          when i = j && lleft = right ->
     284                                let c = gen_or (gen_not c1) c2 in
     285                                Ternary(i, c, lleft, lright)
     286      | Ternary(j, c2, lleft, lright), _
     287        when i = j && lright = right ->
     288        let c = gen_and c1 c2 in
     289        Ternary(i, c, lleft, lright)
     290      | _, Ternary(j, c2, rleft, rright)
     291        when i = j && left = rleft ->
     292        let c = gen_or c1 c2 in
     293        Ternary(i, c, rleft, rright)
     294      | _, Ternary(j, c2, rleft, rright)
     295        when i = j && left = rright ->
     296        let c = gen_and_not c2 c1 in
     297        Ternary(i, c, rleft, rright)
     298                        | _ -> Ternary (i, c1, left, right)
     299
     300let rec chose_smaller_cond = function
     301        | Exact k -> Exact k
     302        | Ternary (i, c, left, right) ->
     303                let left = chose_smaller_cond left in
     304                let right = chose_smaller_cond right in
     305                let c_not = gen_not c in
     306                if CondSet.cardinal c > CondSet.cardinal c_not then
     307                        Ternary (i, c_not, right, left)
     308                else
     309                        Ternary (i, c, left, right)
    268310
    269311let cost_expr_mapping_of_cost_mapping m =
     
    273315                        let e = remove_useless_branches e in
    274316                        let e = remove_useless_branchings e in
     317                        let e = chose_smaller_cond e in
    275318      Atom.Map.add at e in
    276319    Atom.Map.fold f sets Atom.Map.empty
Note: See TracChangeset for help on using the changeset viewer.