Mercurial > urweb

comparison src/iflow.sml @ 1231:5fa8ae2a34e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Avoid pointless rebuilding of hypothesis E-graphs
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:25:45 -0400
parents 8768145eed1e
children efbefd6e3f6c
comparison
equal deleted inserted replaced
1230:8768145eed1e 1231:5fa8ae2a34e3
957 decomp 957 decomp
958 end 958 end
959 959
960 val tabs = ref (SM.empty : (string list * string list list) SM.map) 960 val tabs = ref (SM.empty : (string list * string list list) SM.map)
961 961
962 fun imply (hyps, goals, outs) = 962 fun ccOf hyps =
963 let
964 val cc = Cc.database ()
965 val () = app (fn a => Cc.assert (cc, a)) hyps
966
967 (* Take advantage of table key information *)
968 fun findKeys hyps =
969 case hyps of
970 [] => ()
971 | AReln (Sql tab, [r1]) :: hyps =>
972 (case SM.find (!tabs, tab) of
973 NONE => findKeys hyps
974 | SOME (_, []) => findKeys hyps
975 | SOME (_, ks) =>
976 let
977 fun finder hyps =
978 case hyps of
979 [] => ()
980 | AReln (Sql tab', [r2]) :: hyps =>
981 (if tab' = tab andalso
982 List.exists (List.all (fn f =>
983 let
984 val r =
985 Cc.check (cc,
986 AReln (Eq, [Proj (r1, f),
987 Proj (r2, f)]))
988 in
989 (*Print.prefaces "Fs"
990 [("tab",
991 Print.PD.string tab),
992 ("r1",
993 p_exp (Proj (r1, f))),
994 ("r2",
995 p_exp (Proj (r2, f))),
996 ("r",
997 Print.PD.string
998 (Bool.toString r))];*)
999 r
1000 end)) ks then
1001 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
1002 ("r1", p_exp r1),
1003 ("r2", p_exp r2),
1004 ("rp1", Cc.p_repOf cc r1),
1005 ("rp2", Cc.p_repOf cc r2)];*)
1006 Cc.assert (cc, AReln (Eq, [r1, r2])))
1007 else
1008 ();
1009 finder hyps)
1010 | _ :: hyps => finder hyps
1011 in
1012 finder hyps;
1013 findKeys hyps
1014 end)
1015 | _ :: hyps => findKeys hyps
1016 in
1017 findKeys hyps;
1018 cc
1019 end
1020
1021 fun imply (cc, hyps, goals, outs) =
963 let 1022 let
964 fun gls goals onFail acc = 1023 fun gls goals onFail acc =
965 case goals of 1024 case goals of
966 [] => 1025 [] =>
967 (let 1026 ((List.all (fn a =>
968 val cc = Cc.database () 1027 if Cc.check (cc, a) then
969 val () = app (fn a => Cc.assert (cc, a)) hyps 1028 true
970 1029 else
971 (* Take advantage of table key information *) 1030 ((*Print.prefaces "Can't prove"
972 fun findKeys hyps = 1031 [("a", p_atom a),
973 case hyps of 1032 ("hyps", Print.p_list p_atom hyps),
974 [] => () 1033 ("db", Cc.p_database cc)];*)
975 | AReln (Sql tab, [r1]) :: hyps => 1034 false)) acc
976 (case SM.find (!tabs, tab) of 1035 andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
977 NONE => findKeys hyps 1036 andalso (case outs of
978 | SOME (_, []) => findKeys hyps 1037 NONE => true
979 | SOME (_, ks) => 1038 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
980 let 1039 Base = outs})))
981 fun finder hyps = 1040 handle Cc.Contradiction => false
982 case hyps of 1041 | Cc.Undetermined => false)
983 [] => ()
984 | AReln (Sql tab', [r2]) :: hyps =>
985 (if tab' = tab andalso
986 List.exists (List.all (fn f =>
987 let
988 val r =
989 Cc.check (cc,
990 AReln (Eq, [Proj (r1, f),
991 Proj (r2, f)]))
992 in
993 (*Print.prefaces "Fs"
994 [("tab",
995 Print.PD.string tab),
996 ("r1",
997 p_exp (Proj (r1, f))),
998 ("r2",
999 p_exp (Proj (r2, f))),
1000 ("r",
1001 Print.PD.string
1002 (Bool.toString r))];*)
1003 r
1004 end)) ks then
1005 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
1006 ("r1", p_exp r1),
1007 ("r2", p_exp r2),
1008 ("rp1", Cc.p_repOf cc r1),
1009 ("rp2", Cc.p_repOf cc r2)];*)
1010 Cc.assert (cc, AReln (Eq, [r1, r2])))
1011 else
1012 ();
1013 finder hyps)
1014 | _ :: hyps => finder hyps
1015 in
1016 finder hyps;
1017 findKeys hyps
1018 end)
1019 | _ :: hyps => findKeys hyps
1020 in
1021 findKeys hyps;
1022
1023 (*Print.preface ("db", Cc.p_database cc);*)
1024 (List.all (fn a =>
1025 if Cc.check (cc, a) then
1026 true
1027 else
1028 ((*Print.prefaces "Can't prove"
1029 [("a", p_atom a),
1030 ("hyps", Print.p_list p_atom hyps),
1031 ("db", Cc.p_database cc)];*)
1032 false)) acc
1033 andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
1034 andalso (case outs of
1035 NONE => true
1036 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
1037 Base = outs})))
1038 handle Cc.Contradiction => false
1039 end handle Cc.Undetermined => false)
1040 orelse onFail () 1042 orelse onFail ()
1041 | (g as AReln (Sql gf, [ge])) :: goals => 1043 | (g as AReln (Sql gf, [ge])) :: goals =>
1042 let 1044 let
1043 fun hps hyps = 1045 fun hps hyps =
1044 case hyps of 1046 case hyps of
1071 in 1073 in
1072 reset (); 1074 reset ();
1073 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps), 1075 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
1074 ("goals", Print.p_list p_atom goals)];*) 1076 ("goals", Print.p_list p_atom goals)];*)
1075 gls goals (fn () => false) [] 1077 gls goals (fn () => false) []
1076 end handle Cc.Contradiction => true 1078 end
1077 1079
1078 fun patCon pc = 1080 fun patCon pc =
1079 case pc of 1081 case pc of
1080 PConVar n => "C" ^ Int.toString n 1082 PConVar n => "C" ^ Int.toString n
1081 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 1083 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
2469 2471
2470 fun doDml (cmds, pols) = 2472 fun doDml (cmds, pols) =
2471 app (fn (loc, p) => 2473 app (fn (loc, p) =>
2472 if decompH p 2474 if decompH p
2473 (fn hyps => 2475 (fn hyps =>
2474 List.exists (fn p' => 2476 let
2475 if decompG p' 2477 val cc = ccOf hyps
2476 (fn goals => imply (hyps, goals, NONE)) then 2478 in
2477 ((*reset (); 2479 List.exists (fn p' =>
2478 Print.prefaces "Match" [("hyp", p_prop p), 2480 if decompG p'
2479 ("goal", p_prop p')];*) 2481 (fn goals => imply (cc, hyps, goals, NONE)) then
2480 true) 2482 ((*reset ();
2481 else 2483 Print.prefaces "Match" [("hyp", p_prop p),
2482 false) 2484 ("goal", p_prop p')];*)
2483 pols) then 2485 true)
2486 else
2487 false)
2488 pols
2489 end handle Cc.Contradiction => true) then
2484 () 2490 ()
2485 else 2491 else
2486 (ErrorMsg.errorAt loc "The information flow policy may be violated here."; 2492 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
2487 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds 2493 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
2488 in 2494 in
2493 val p = And (p, Reln (Eq, [Var 0, e])) 2499 val p = And (p, Reln (Eq, [Var 0, e]))
2494 in 2500 in
2495 if decompH p 2501 if decompH p
2496 (fn hyps => 2502 (fn hyps =>
2497 let 2503 let
2504 val cc = ccOf hyps
2505
2498 val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab) 2506 val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab)
2499 | (_, avail) => avail) SS.empty hyps 2507 | (_, avail) => avail) SS.empty hyps
2500 2508
2501 fun tryCombos (maxLv, pols, g, outs) = 2509 fun tryCombos (maxLv, pols, g, outs) =
2502 case pols of 2510 case pols of
2503 [] => 2511 [] =>
2504 decompG g 2512 decompG g
2505 (fn goals => imply (hyps, goals, SOME outs)) 2513 (fn goals => imply (cc, hyps, goals, SOME outs))
2506 | (g1, outs1) :: pols => 2514 | (g1, outs1) :: pols =>
2507 let 2515 let
2508 val g1 = bumpLvarsP (maxLv + 1) g1 2516 val g1 = bumpLvarsP (maxLv + 1) g1
2509 val outs1 = map (bumpLvars (maxLv + 1)) outs1 2517 val outs1 = map (bumpLvars (maxLv + 1)) outs1
2510 fun skip () = tryCombos (maxLv, pols, g, outs) 2518 fun skip () = tryCombos (maxLv, pols, g, outs)
2522 else 2530 else
2523 skip () 2531 skip ()
2524 end 2532 end
2525 in 2533 in
2526 (fl <> Control Where 2534 (fl <> Control Where
2527 andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) 2535 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
2528 orelse List.exists (fn (p', outs) => 2536 orelse List.exists (fn (p', outs) =>
2529 decompG p' 2537 decompG p'
2530 (fn goals => imply (hyps, goals, SOME outs))) 2538 (fn goals => imply (cc, hyps, goals,
2539 SOME outs)))
2531 client 2540 client
2532 orelse tryCombos (0, client, True, []) 2541 orelse tryCombos (0, client, True, [])
2533 orelse (reset (); 2542 orelse (reset ();
2534 Print.preface ("Untenable hypotheses" 2543 Print.preface ("Untenable hypotheses"
2535 ^ (case fl of 2544 ^ (case fl of
2536 Control Where => " (WHERE clause)" 2545 Control Where => " (WHERE clause)"
2537 | Control Case => " (case discriminee)" 2546 | Control Case => " (case discriminee)"
2538 | Data => " (returned data value)"), 2547 | Data => " (returned data value)"),
2539 Print.p_list p_atom hyps); 2548 Print.p_list p_atom hyps);
2540 false) 2549 false)
2541 end) then 2550 end handle Cc.Contradiction => true) then
2542 () 2551 ()
2543 else 2552 else
2544 ErrorMsg.errorAt loc "The information flow policy may be violated here." 2553 ErrorMsg.errorAt loc "The information flow policy may be violated here."
2545 end 2554 end
2546 2555
2575 handle ex => (Settings.setMonoInline oldInline; 2584 handle ex => (Settings.setMonoInline oldInline;
2576 raise ex) 2585 raise ex)
2577 end 2586 end
2578 2587
2579 end 2588 end
2580