engine/ctlcocci_integration.ml

   1 (*
   2  * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
   3  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   4  * This file is part of Coccinelle.
   5  *
   6  * Coccinelle is free software: you can redistribute it and/or modify
   7  * it under the terms of the GNU General Public License as published by
   8  * the Free Software Foundation, according to version 2 of the License.
   9  *
  10  * Coccinelle is distributed in the hope that it will be useful,
  11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13  * GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License
  16  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  17  *
  18  * The authors reserve the right to distribute this or future versions of
  19  * Coccinelle under other licenses.
  20  *)
  21
  22
  23 (*
  24  * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
  25  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
  26  * This file is part of Coccinelle.
  27  *
  28  * Coccinelle is free software: you can redistribute it and/or modify
  29  * it under the terms of the GNU General Public License as published by
  30  * the Free Software Foundation, according to version 2 of the License.
  31  *
  32  * Coccinelle is distributed in the hope that it will be useful,
  33  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  34  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  35  * GNU General Public License for more details.
  36  *
  37  * You should have received a copy of the GNU General Public License
  38  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  39  *
  40  * The authors reserve the right to distribute this or future versions of
  41  * Coccinelle under other licenses.
  42  *)
  43
  44
  45 open Common
  46
  47 open Ograph_extended
  48
  49 module F = Control_flow_c
  50
  51 (*****************************************************************************)
  52 (* Debugging functions *)
  53 (*****************************************************************************)
  54 let show_or_not_predicate pred =
  55   if !Flag_matcher.debug_engine then begin
  56     indent_do (fun () ->
  57       adjust_pp_with_indent_and_header "labeling: pred = " (fun () ->
  58         Pretty_print_engine.pp_predicate pred;
  59       );
  60     )
  61   end
  62
  63 let show_or_not_nodes nodes =
  64   if !Flag_matcher.debug_engine  then begin
  65     indent_do (fun () ->
  66       adjust_pp_with_indent_and_header "labeling: result = " (fun () ->
  67         Common.pp_do_in_box (fun () ->
  68           pp "{";
  69           Common.print_between
  70             (fun () -> pp ";"; Format.print_cut())
  71             (fun (nodei, (_predTODO, subst)) ->
  72               Format.print_int nodei;
  73               Common.pp_do_in_box (fun () ->
  74                 Pretty_print_engine.pp_binding2_ctlsubst subst
  75               )
  76             ) nodes;
  77           pp "}";
  78         );
  79       )
  80     )
  81   end
  82
  83 let show_isos rule_elem =
  84   match Ast_cocci.get_isos rule_elem with
  85     [] -> ()
  86   | isos ->
  87       let line = Ast_cocci.get_line rule_elem in
  88       Printf.printf "rule elem: ";
  89       Pretty_print_cocci.rule_elem "" rule_elem;
  90       Format.print_newline();
  91       List.iter
  92         (function (nm,x) ->
  93           Printf.printf "    iso: %s(%d): " nm line;
  94           Pretty_print_cocci.pp_print_anything x;
  95           Format.print_newline())
  96         isos
  97
  98 (*****************************************************************************)
  99 (* Labeling function *)
 100 (*****************************************************************************)
 101 let (-->) x v = Ast_ctl.Subst (x,v);;
 102
 103 (* Take list of predicate and for each predicate returns where in the
 104  * control flow it matches, and the set of subsitutions for this match.
 105  *)
 106 let (labels_for_ctl: string list (* dropped isos *) ->
 107  (nodei * F.node) list -> Lib_engine.metavars_binding ->
 108  Lib_engine.label_ctlcocci) =
 109   fun dropped_isos nodes binding ->
 110
 111    (fun p ->
 112      show_or_not_predicate p;
 113
 114      let nodes' = nodes +> List.map (fun (nodei, node) ->
 115       (* todo? put part of this code in pattern ? *)
 116       (match p, F.unwrap node with
 117       | Lib_engine.Paren s,  (F.SeqStart (_, bracelevel, _)) ->
 118           let make_var x = ("",i_to_s x) in
 119           [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
 120       | Lib_engine.Paren s,  (F.SeqEnd (bracelevel, _)) ->
 121           let make_var x = ("",i_to_s x) in
 122           [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
 123       | Lib_engine.Paren _, _ -> []
 124       | Lib_engine.Label s, _ ->
 125           let labels = F.extract_labels node in
 126           [(nodei,
 127             (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))]
 128       | Lib_engine.BCLabel s, _ ->
 129           (match F.extract_bclabels node with
 130             [] -> [] (* null for all nodes that are not break or continue *)
 131           | labels ->
 132               [(nodei,
 133                 (p,[(s -->
 134                   (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))])
 135       | Lib_engine.PrefixLabel s, _ ->
 136           let labels = F.extract_labels node in
 137           [(nodei,
 138             (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))]
 139
 140       | Lib_engine.Match (re), _unwrapnode ->
 141           let substs =
 142             Pattern_c.match_re_node dropped_isos re node binding
 143             +> List.map (fun (re', subst) ->
 144               Lib_engine.Match (re'), subst
 145             )
 146           in
 147           substs +> List.map (fun (p', subst) ->
 148             (nodei,
 149               (p',
 150                 subst +> List.map (fun (s, meta) ->
 151                   s --> Lib_engine.NormalMetaVal meta
 152                 ))))
 153
 154       | Lib_engine.InLoop,      F.InLoopNode ->  [nodei, (p,[])]
 155       | Lib_engine.TrueBranch , F.TrueNode ->  [nodei, (p,[])]
 156       | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])]
 157       | Lib_engine.After,       F.AfterNode -> [nodei, (p,[])]
 158       | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])]
 159       | Lib_engine.LoopFallThrough, F.LoopFallThroughNode -> [nodei,(p,[])]
 160       | Lib_engine.FunHeader,   F.FunHeader _ -> [nodei, (p,[])]
 161       | Lib_engine.Top,         F.TopNode ->   [nodei, (p,[])]
 162       | Lib_engine.Exit,        F.Exit ->      [nodei, (p,[])]
 163       | Lib_engine.ErrorExit,   F.ErrorExit -> [nodei, (p,[])]
 164       | Lib_engine.Goto,        F.Goto(_,_,_) -> [nodei, (p,[])]
 165
 166       | Lib_engine.InLoop , _ -> []
 167       | Lib_engine.TrueBranch , _ -> []
 168       | Lib_engine.FalseBranch, _ -> []
 169       | Lib_engine.After, _ -> []
 170       | Lib_engine.FallThrough, _ -> []
 171       | Lib_engine.LoopFallThrough, _ -> []
 172       | Lib_engine.FunHeader, _  -> []
 173       | Lib_engine.Top, _  -> []
 174       | Lib_engine.Exit, _  -> []
 175       | Lib_engine.ErrorExit, _  -> []
 176       | Lib_engine.Goto, _  -> []
 177
 178       | Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))]
 179       | Lib_engine.BindBad s, _ ->  [(nodei, (p,[(s --> Lib_engine.BadVal)]))]
 180       | Lib_engine.FakeBrace, _ ->
 181           if F.extract_is_fake node then [nodei, (p,[])] else []
 182
 183       | Lib_engine.Return, node ->
 184           (match node with
 185             (* todo? should match the Exit code ?
 186              * todo: one day try also to match the special function
 187              * such as panic();
 188              *)
 189           | F.Return _ ->  [nodei, (p,[])]
 190           | F.ReturnExpr _ -> [nodei, (p,[])]
 191           | _ -> []
 192           )
 193       )
 194      ) +> List.concat
 195      in
 196
 197      show_or_not_nodes nodes';
 198      nodes'
 199    )
 200
 201 (*****************************************************************************)
 202 (* Some fix flow, for CTL, for unparse *)
 203 (*****************************************************************************)
 204 (* could erase info on nodes, and edge, because they are not used by rene *)
 205 let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) =
 206  fun cflow -> cflow
 207
 208
 209
 210 (* Just make the final node of the control flow loop over itself.
 211  * It seems that one hypothesis of the SAT algorithm is that each node as at
 212  * least a successor.
 213  *
 214  * update: do same for errorexit node.
 215  *
 216  * update: also erase the fake nodes (and adjust the edges accordingly),
 217  * so that AX in CTL can now work.
 218  * Indeed, à la fin de la branche then (et else), on devrait aller directement
 219  * au suivant du endif, sinon si ecrit if(1) { foo(); }; bar();
 220  * sans '...' entre le if et bar(), alors ca matchera pas car le CTL
 221  * generera un AX bar()  qui il tombera d'abord sur le [endif] :(
 222  * Mais chiant de changer l'algo de generation, marche pas tres bien avec
 223  * ma facon de faire recursive et compositionnel.
 224  * => faire une fonction qui applique des fixes autour de ce control flow,
 225  * comme ca passe un bon flow a rene, mais garde un flow a moi pour pouvoir
 226  * facilement generate back the ast.
 227  * alt: faire un wrapper autourde mon graphe pour lui passer dans le module CFG
 228  * une fonction qui passe a travers les Fake, mais bof.
 229  *
 230  * update: also make loop the deadcode nodes, the one that have
 231  * no predecessor.
 232  *)
 233 let (fix_flow_ctl2: F.cflow -> F.cflow) = fun flow ->
 234   let g = ref flow in
 235
 236   let topi = F.first_node !g in
 237   !g#add_arc ((topi, topi), F.Direct);
 238
 239   (* for the #define CFG who have no Exit but have at least a EndNode *)
 240   (try
 241       let endi  = F.find_node (fun x -> x =*= F.EndNode) !g in
 242       !g#add_arc ((endi, endi), F.Direct);
 243     with Not_found -> ()
 244   );
 245
 246   (* for the regular functions *)
 247   (try
 248     let exitnodei  = F.find_node (fun x -> x =*= F.Exit) !g in
 249     let errornodei = F.find_node (fun x -> x =*= F.ErrorExit) !g in
 250
 251     !g#add_arc ((exitnodei, exitnodei), F.Direct);
 252
 253     if null ((!g#successors   errornodei)#tolist) &&
 254        null ((!g#predecessors errornodei)#tolist)
 255     then !g#del_node errornodei
 256     else !g#add_arc ((errornodei, errornodei), F.Direct);
 257    with Not_found -> ()
 258   );
 259
 260   let fake_nodes = !g#nodes#tolist +> List.filter (fun (nodei, node) ->
 261     match F.unwrap node with
 262     | F.CaseNode _
 263     | F.Enter
 264     (*| F.Fake*) (* [endif], [endswitch], ... *)
 265       -> true
 266     | _ -> false
 267     ) in
 268
 269   fake_nodes +> List.iter (fun (nodei, node) -> F.remove_one_node nodei !g);
 270
 271   (* even when have deadcode, julia want loop over those nodes *)
 272   !g#nodes#tolist +> List.iter (fun (nodei, node) ->
 273     if (!g#predecessors nodei)#null
 274     then begin
 275       let fakei = !g#add_node (F.mk_node F.Fake [] [] "DEADCODELOOP") in
 276       !g#add_arc ((fakei, nodei), F.Direct);
 277       !g#add_arc ((fakei, fakei), F.Direct);
 278     end
 279   );
 280
 281   !g#nodes#tolist +> List.iter (fun (nodei, node) ->
 282     assert (List.length ((!g#successors nodei)#tolist) >= 1);
 283     (* no:  && List.length ((!g#predecessors nodei)#tolist) >= 1
 284        because    the enter node at least have no predecessors *)
 285     );
 286
 287   !g
 288 let fix_flow_ctl a =
 289   Common.profile_code "fix_flow" (fun () -> fix_flow_ctl2 a)
 290
 291
 292
 293
 294
 295 (*****************************************************************************)
 296 (* subtil: the label must operate on newflow, not (old) cflow
 297  * update: now I supposed that we give me a fixed_flow
 298  *)
 299 let model_for_ctl dropped_isos cflow binding =
 300  let newflow = cflow (* old: fix_flow_ctl (control_flow_for_ctl cflow) *) in
 301  let labels = labels_for_ctl dropped_isos (newflow#nodes#tolist) binding  in
 302  let states = List.map fst  newflow#nodes#tolist  in
 303  newflow, labels, states
 304
 305
 306 (*****************************************************************************)
 307
 308 module PRED =
 309   struct
 310     type t = Lib_engine.predicate
 311     let print_predicate x =
 312       Pretty_print_cocci.print_plus_flag := false;
 313       Pretty_print_cocci.print_minus_flag := false;
 314       Pretty_print_engine.pp_predicate x
 315   end
 316
 317 (* prefix has to be nonempty *)
 318 let prefix l1 l2 =
 319   let rec loop = function
 320       ([],_) -> true
 321     | (_,[]) -> false
 322     | (x::xs,y::ys) when x = y -> loop (xs,ys)
 323     | _ -> false in
 324   loop(l1,l2)
 325
 326 let compatible_labels l1 l2 =
 327   match (l1,l2) with
 328     (Lib_engine.Absolute(l1),Lib_engine.Absolute(l2)) -> l1 =*= l2
 329   | (Lib_engine.Absolute(l1),Lib_engine.Prefix(l2))   -> prefix l1 l2
 330   | (Lib_engine.Prefix(l1),Lib_engine.Absolute(l2))   -> prefix l2 l1
 331   | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2))     ->
 332       not (l1 = []) && not (l2 = []) &&
 333       List.hd l1 =*= List.hd l2 (* labels are never empty *)
 334
 335 let merge_labels l1 l2 =
 336   match (l1,l2) with
 337     (* known to be compatible *)
 338     (Lib_engine.Absolute(_),Lib_engine.Absolute(_)) -> l1
 339   | (Lib_engine.Absolute(_),Lib_engine.Prefix(_))   -> l1
 340   | (Lib_engine.Prefix(_),Lib_engine.Absolute(_))   -> l2
 341   | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2))   ->
 342       let rec max_prefix = function
 343           (x::xs,y::ys) when x = y -> x::(max_prefix(xs,ys))
 344         | (l1,l2) -> [] in
 345       Lib_engine.Prefix(max_prefix(l1,l2))
 346
 347 module ENV =
 348   struct
 349     type value = Lib_engine.metavar_binding_kind2
 350     type mvar = Ast_cocci.meta_name
 351     let eq_mvar x x' = x =*= x'
 352     let eq_val v v' =
 353       (* v = v' *)
 354       match (v,v') with
 355         (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
 356          Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
 357            ((min1 <= min2) && (max1 >= max2)) or
 358            ((min2 <= min1) && (max2 >= max1))
 359       | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
 360          Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
 361           C_vs_c.eq_type a b
 362       | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
 363           compatible_labels l1 l2
 364       | _ -> v =*= v'
 365     let merge_val v v' = (* values guaranteed to be compatible *)
 366       (* v *)
 367       match (v,v') with
 368         (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
 369          Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
 370            if (min1 <= min2) && (max1 >= max2)
 371            then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1))
 372            else
 373              if (min2 <= min1) && (max2 >= max1)
 374              then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))
 375              else failwith "incompatible positions give to merge"
 376       | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
 377          Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
 378           Lib_engine.NormalMetaVal (Ast_c.MetaTypeVal (C_vs_c.merge_type a b))
 379       | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
 380           Lib_engine.LabelVal(merge_labels l1 l2)
 381
 382       | _ -> v
 383     let print_mvar (_,s) = Format.print_string s
 384     let print_value x = Pretty_print_engine.pp_binding_kind2 x
 385   end
 386
 387 module CFG =
 388   struct
 389     type node = Ograph_extended.nodei
 390     type cfg = (F.node, F.edge) Ograph_extended.ograph_mutable
 391     let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist)
 392     let successors   cfg n = List.map fst ((cfg#successors n)#tolist)
 393     let extract_is_loop cfg n =
 394       Control_flow_c.extract_is_loop (cfg#nodes#find n)
 395     let print_node i = Format.print_string (i_to_s i)
 396     let size cfg = cfg#nodes#length
 397
 398     (* In ctl_engine, we use 'node' for the node but in the Ograph_extended
 399      * terminology, this 'node' is in fact an index to access the real
 400      * node information (that ctl/ wants to abstract away to be more generic),
 401      * the 'Ograph_extended.nodei'.
 402      *)
 403     let print_graph cfg label border_colors fill_colors filename =
 404       Ograph_extended.print_ograph_mutable_generic cfg label
 405         (fun (nodei, (node: F.node)) ->
 406           (* the string julia wants to put ? *)
 407           let bc = try Some(List.assoc nodei border_colors) with _ -> None in
 408           let fc = try Some(List.assoc nodei fill_colors) with _ -> None in
 409           (* the string yoann put as debug information in the cfg *)
 410           let str = snd node in
 411           (str,bc,fc)
 412         )
 413         ~output_file:filename
 414         ~launch_gv:false
 415   end
 416
 417
 418 module WRAPPED_ENGINE = Wrapper_ctl.CTL_ENGINE_BIS (ENV) (CFG) (PRED)
 419
 420 let print_bench _ = WRAPPED_ENGINE.print_bench()
 421
 422 type pred = Lib_engine.predicate * Ast_cocci.meta_name Ast_ctl.modif
 423
 424 (*****************************************************************************)
 425 let metavars_binding2_to_binding   binding2 =
 426   binding2 +> Common.map_filter (fun (s, kind2) ->
 427     match kind2 with
 428     | Lib_engine.NormalMetaVal kind -> Some (s, kind)
 429     (* I thought it was Impossible to have this when called from
 430        satbis_to_trans_info but it does not seems so *)
 431     | Lib_engine.ParenVal _ -> None
 432     | Lib_engine.LabelVal _ -> None
 433     | Lib_engine.BadVal     -> None (* should not occur *)
 434     | Lib_engine.GoodVal    -> None (* should not occur *)
 435    )
 436
 437 let metavars_binding_to_binding2 binding =
 438   binding +> List.map (fun (s, kind) -> s, Lib_engine.NormalMetaVal kind)
 439
 440
 441 let (satbis_to_trans_info:
 442   (int list *
 443      (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate)) list ->
 444   (int list *
 445      (nodei * Lib_engine.metavars_binding * Ast_cocci.rule_elem)) list) =
 446   fun xs ->
 447     xs +> List.fold_left (fun prev (index,(nodei, binding2, pred)) ->
 448       match pred with
 449       | Lib_engine.Match (rule_elem) ->
 450           if !Flag.track_iso_usage then show_isos rule_elem;
 451           (index,
 452            (nodei, metavars_binding2_to_binding binding2, rule_elem))
 453           ::prev
 454              (* see BindGood in asttotctl2 *)
 455       | Lib_engine.BindGood (_) -> prev
 456       | _ -> raise Impossible
 457     ) []
 458
 459 (*****************************************************************************)
 460
 461 let rec coalesce_positions = function
 462     [] -> []
 463   | (x,Ast_c.MetaPosValList l)::rest ->
 464       let (same,others) = List.partition (function (x1,_) -> x =*= x1) rest in
 465       let ls =
 466         List.concat
 467           (List.map
 468              (function
 469                  (_,Ast_c.MetaPosValList l) -> l
 470                | _ -> failwith "unexpected non-position")
 471              same) in
 472       let new_ls = List.sort compare (l@ls) in
 473       (x,Ast_c.MetaPosValList new_ls) :: coalesce_positions others
 474   | x::rest -> x :: coalesce_positions rest
 475
 476 let strip env =
 477   List.map
 478     (function (v,vl) ->
 479       let vl =
 480         match vl with
 481           Ast_c.MetaExprVal (a,c) ->
 482             Ast_c.MetaExprVal(Lib_parsing_c.al_inh_expr a,c)
 483         | Ast_c.MetaExprListVal a ->
 484             Ast_c.MetaExprListVal(Lib_parsing_c.al_inh_arguments a)
 485         | Ast_c.MetaStmtVal a ->
 486             Ast_c.MetaStmtVal(Lib_parsing_c.al_inh_statement a)
 487         | Ast_c.MetaInitVal a ->
 488             Ast_c.MetaInitVal(Lib_parsing_c.al_inh_init a)
 489         | x -> (*don't contain binding info*) x in
 490       (v,vl))
 491     env
 492
 493 let rec nub ls =
 494   match ls with
 495     [] -> []
 496   | (x::xs) when (List.mem x xs) -> nub xs
 497   | (x::xs) -> x::(nub xs)
 498
 499 (*****************************************************************************)
 500 (* Call ctl engine *)
 501 (*****************************************************************************)
 502 let (mysat2:
 503   Lib_engine.model ->
 504   (Lib_engine.ctlcocci * (pred list list)) ->
 505   (Lib_engine.mvar list*Lib_engine.metavars_binding) ->
 506   (Lib_engine.numbered_transformation_info * bool *
 507      Lib_engine.metavars_binding * Lib_engine.metavars_binding list)) =
 508   fun (flow, label, states) ctl (used_after, binding) ->
 509     let binding2 = metavars_binding_to_binding2 binding in
 510     let (triples,(trans_info2, returned_any_states, used_after_envs)) =
 511       WRAPPED_ENGINE.satbis (flow, label, states) ctl
 512         (used_after, binding2)
 513     in
 514     if not (!Flag_parsing_cocci.sgrep_mode || !Flag.sgrep_mode2 ||
 515             !Flag_matcher.allow_inconsistent_paths)
 516     then Check_reachability.check_reachability triples flow;
 517     let (trans_info2,used_after_fresh_envs) =
 518       Postprocess_transinfo.process used_after binding2 trans_info2 in
 519     let used_after_envs =
 520       Common.uniq(List.map2 (@) used_after_fresh_envs used_after_envs) in
 521     let trans_info = satbis_to_trans_info trans_info2 in
 522     let newbindings = List.map metavars_binding2_to_binding used_after_envs in
 523     let newbindings = List.map coalesce_positions newbindings in
 524     let newbindings = List.map strip newbindings in
 525     let newbindings = nub newbindings in
 526     (trans_info, returned_any_states, binding, newbindings)
 527
 528 let mysat a b c =
 529   Common.profile_code "mysat" (fun () -> mysat2 a b c)