let ctl_seqor x y =
match (x,y) with
- (CTL.True,_) | (_,CTL.True) -> CTL.True
+ (* drop x or true case because x might have side effects *)
+ (CTL.True,_) (* | (_,CTL.True) *) -> CTL.True
| (CTL.False,a) | (a,CTL.False) -> a
| _ -> CTL.SeqOr(x,y)
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing stmtdotsfn donothing
+ donothing donothing stmtdotsfn donothing donothing
donothing donothing donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing
let init r k i =
let res = k i in
match Ast.unwrap i with
- Ast.InitList(allminus,_,_,_,_) -> allminus or res
+ Ast.StrInitList(allminus,_,_,_,_) -> allminus or res
| _ -> res in
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing do_nothing do_nothing do_nothing init do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
| _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
let make_raw_match label guard code =
- predmaker guard (Lib_engine.Match(code),CTL.Control) label
+ match intersect !used_after (Ast.get_fvs code) with
+ [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label
+ | _ ->
+ let v = fresh_var() in
+ CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v)
+ label)
let rec seq_fvs quantified = function
[] -> []
let mcode r x = 0 in
let recursor = V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing donothing donothing
+ donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing donothing
donothing donothing stmt_count donothing donothing donothing in
let res = string_of_int (recursor.V.combiner_statement s) in
let e1 = get_whencond_exps e in
let (if_headers, while_headers, for_headers) =
make_whencond_headers e e1 label guard quantified in
+ (* if with else *)
ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
- (ctl_and CTL.NONSTRICT (loopfallpred label)
- (ctl_or (ctl_back_ex if_headers)
+ (* if without else *)
+ (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers))
+ (* failure of loop test *)
+ (ctl_and CTL.NONSTRICT (loopfallpred label)
(ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
(* --------------------------------------------------------------------- *)
let (lbfvs,b1fvs,b2fvs,rbfvs) =
match
seq_fvs quantified
- [Ast.get_fvs lbrace;
- Ast.get_fvs body;Ast.get_fvs rbrace]
+ [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace]
with
- [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
- (lbfvs,b1fvs,b2fvs,rbfvs)
+ [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs)
| _ -> failwith "not possible" in
let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) =
match
seq_fvs minus_quantified
- [Ast.get_mfvs lbrace;
- Ast.get_mfvs body;Ast.get_mfvs rbrace]
+ [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace]
with
[(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
(lbfvs,b1fvs,b2fvs,rbfvs)
(* label is not needed; paren_pred is enough *)
quantify guard rbfvs
(ctl_au (make_match empty_rbrace)
- (ctl_and
- (real_make_match None guard rbrace)
- paren_pred)) in
+ (ctl_and (real_make_match None guard rbrace) paren_pred)) in
let new_quantified2 =
Common.union_set b1fvs (Common.union_set b2fvs quantified) in
let new_mquantified2 =
new_quantified2 new_mquantified2
(Some (lv,ref true))
llabel slabel false guard)))])) in
- if ends_in_return body
+ let empty_body =
+ match Ast.undots body with
+ [body] ->
+ (match Ast.unwrap body with
+ Ast.Dots
+ ((_,i,Ast.CONTEXT(_,Ast.NOTHING),_),[],_,_) ->
+ (match Ast.unwrap rbrace with
+ Ast.SeqEnd((_,_,Ast.CONTEXT(_,Ast.NOTHING),_))
+ when not (contains_pos rbrace) -> true
+ | _ -> false)
+ | _ -> false)
+ | _ -> false in
+ if empty_body && after = Tail
+ (* for just a match of an if branch of the form { ... }, just
+ match the first brace *)
+ then quantify guard lbfvs (make_match lbrace)
+ else if ends_in_return body
then
(* matching error handling code *)
(* Cases:
| Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) ->
(* label in recursive call is None because label check is already
- wrapped around the corresponding code *)
+ wrapped around the corresponding code. not good enough, want to stay
+ in a specific region, dots and nests will keep going *)
let bfvs =
match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
quantify guard bfvs
(let dots_pattern =
statement_list stmt_dots (a2n after) new_quantified minus_quantified
- None llabel slabel true guard in
+ label(*None*) llabel slabel true guard in
dots_and_nests multi
(Some dots_pattern) whencode bef aft dot_code after label
(process_bef_aft new_quantified minus_quantified
- None llabel slabel true)
+ label(*None*) llabel slabel true)
(function x ->
- statement_list x Tail new_quantified minus_quantified None
+ statement_list x Tail new_quantified minus_quantified label(*None*)
llabel slabel true true)
(function x ->
- statement x Tail new_quantified minus_quantified None
+ statement x Tail new_quantified minus_quantified label(*None*)
llabel slabel true)
guard quantified
(function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
(match d with
Ast.MINUS(_,_,_,_) -> None
| _ ->
+ let pv =
+ (* no nested braces, because only dots *)
+ string2var ("p1") in
+ let paren_pred =
+ CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
Some (
make_seq
- [start_brace;
+ [ctl_and start_brace paren_pred;
match whencode with
[] -> CTL.True
| _ ->
CTL.True
| Ast.WhenModifier(_) -> prev)
CTL.True whencode) in
- ctl_au leftarg (make_match stripped_rbrace)]))
+ ctl_au leftarg
+ (ctl_and
+ (make_match stripped_rbrace)
+ paren_pred)]))
| _ -> None)
| _ -> None in
let optim2 =