Mercurial > urweb

comparison src/iflow.sml @ 1218:48d2ca496d2c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Path conditions, used to track implicit flows
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 13:02:15 -0400
parents 4d206e603300
children 3224faec752d
comparison
equal deleted inserted replaced
1217:4d206e603300 1218:48d2ca496d2c
378 | _ => false 378 | _ => false
379 379
380 (* Congruence closure *) 380 (* Congruence closure *)
381 structure Cc :> sig 381 structure Cc :> sig
382 type database 382 type database
383 type representative
384 383
385 exception Contradiction 384 exception Contradiction
386 exception Undetermined 385 exception Undetermined
387 386
388 val database : unit -> database 387 val database : unit -> database
389 val representative : database * exp -> representative
390 388
391 val assert : database * atom -> unit 389 val assert : database * atom -> unit
392 val check : database * atom -> bool 390 val check : database * atom -> bool
393 391
394 val p_database : database Print.printer 392 val p_database : database Print.printer
393
394 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
395 end = struct 395 end = struct
396 396
397 exception Contradiction 397 exception Contradiction
398 exception Undetermined 398 exception Undetermined
399 399
418 type representative = node ref 418 type representative = node ref
419 419
420 val finish = ref (Node {Rep = ref NONE, 420 val finish = ref (Node {Rep = ref NONE,
421 Cons = ref SM.empty, 421 Cons = ref SM.empty,
422 Variety = VFinish, 422 Variety = VFinish,
423 Known = ref false}) 423 Known = ref true})
424 424
425 type database = {Vars : representative IM.map ref, 425 type database = {Vars : representative IM.map ref,
426 Consts : representative CM.map ref, 426 Consts : representative CM.map ref,
427 Con0s : representative SM.map ref, 427 Con0s : representative SM.map ref,
428 Records : (representative SM.map * representative) list ref, 428 Records : (representative SM.map * representative) list ref,
468 newline, 468 newline,
469 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i), 469 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
470 space, 470 space,
471 string "=", 471 string "=",
472 space, 472 space,
473 p_rep n]) (IM.listItemsi (!(#Vars db)))] 473 p_rep n,
474 if !(#Known (unNode n)) then
475 box [space,
476 string "(known)"]
477 else
478 box []]) (IM.listItemsi (!(#Vars db)))]
474 479
475 fun repOf (n : representative) : representative = 480 fun repOf (n : representative) : representative =
476 case !(#Rep (unNode n)) of 481 case !(#Rep (unNode n)) of
477 NONE => n 482 NONE => n
478 | SOME r => 483 | SOME r =>
482 #Rep (unNode n) := SOME r; 487 #Rep (unNode n) := SOME r;
483 r 488 r
484 end 489 end
485 490
486 fun markKnown r = 491 fun markKnown r =
487 (#Known (unNode r) := true; 492 if !(#Known (unNode r)) then
488 case #Variety (unNode r) of 493 ()
489 Dt1 (_, r) => markKnown r 494 else
490 | Recrd xes => SM.app markKnown (!xes) 495 (#Known (unNode r) := true;
491 | _ => ()) 496 SM.app markKnown (!(#Cons (unNode r)));
497 case #Variety (unNode r) of
498 Dt1 (_, r) => markKnown r
499 | Recrd xes => SM.app markKnown (!xes)
500 | _ => ())
492 501
493 fun representative (db : database, e) = 502 fun representative (db : database, e) =
494 let 503 let
495 fun rep e = 504 fun rep e =
496 case e of 505 case e of
527 | NONE => 536 | NONE =>
528 let 537 let
529 val r = ref (Node {Rep = ref NONE, 538 val r = ref (Node {Rep = ref NONE,
530 Cons = ref SM.empty, 539 Cons = ref SM.empty,
531 Variety = Dt0 f, 540 Variety = Dt0 f,
532 Known = ref false}) 541 Known = ref true})
533 in 542 in
534 #Con0s db := SM.insert (!(#Con0s db), f, r); 543 #Con0s db := SM.insert (!(#Con0s db), f, r);
535 r 544 r
536 end) 545 end)
537 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0" 546 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
745 in 754 in
746 unif (!xes1, !xes2); 755 unif (!xes1, !xes2);
747 unif (!xes2, !xes1) 756 unif (!xes2, !xes1)
748 end 757 end
749 | (VFinish, VFinish) => () 758 | (VFinish, VFinish) => ()
750 | (Nothing, _) => 759 | (Nothing, _) => mergeNodes (r1, r2)
751 (#Rep (unNode r1) := SOME r2; 760 | (_, Nothing) => mergeNodes (r2, r1)
752 if !(#Known (unNode r1)) andalso not (!(#Known (unNode r2))) then
753 markKnown r2
754 else
755 ();
756 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
757 compactFuncs ())
758 | (_, Nothing) =>
759 (#Rep (unNode r2) := SOME r1;
760 if !(#Known (unNode r2)) andalso not (!(#Known (unNode r1))) then
761 markKnown r1
762 else
763 ();
764 #Cons (unNode r1) := SM.unionWith #1 (!(#Cons (unNode r1)), !(#Cons (unNode r2)));
765 compactFuncs ())
766 | _ => raise Contradiction 761 | _ => raise Contradiction
762
763 and mergeNodes (r1, r2) =
764 (#Rep (unNode r1) := SOME r2;
765 if !(#Known (unNode r1)) then
766 markKnown r2
767 else
768 ();
769 if !(#Known (unNode r2)) then
770 markKnown r1
771 else
772 ();
773 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
774 compactFuncs ())
767 775
768 and compactFuncs () = 776 and compactFuncs () =
769 let 777 let
770 fun loop funcs = 778 fun loop funcs =
771 case funcs of 779 case funcs of
813 in 821 in
814 repOf r1 = repOf r2 822 repOf r1 = repOf r2
815 end 823 end
816 | _ => false 824 | _ => false
817 825
826 fun builtFrom (db, {Base = bs, Derived = d}) =
827 let
828 val bs = map (fn b => representative (db, b)) bs
829
830 fun loop d =
831 let
832 val d = repOf d
833 in
834 List.exists (fn b => repOf b = d) bs
835 orelse case #Variety (unNode d) of
836 Dt0 _ => true
837 | Dt1 (_, d) => loop d
838 | Prim _ => true
839 | Recrd xes => List.all loop (SM.listItems (!xes))
840 | VFinish => true
841 | Nothing => false
842 end
843 in
844 loop (representative (db, d))
845 end
846
818 end 847 end
819 848
820 fun decomp fals or = 849 fun decomp fals or =
821 let 850 let
822 fun decomp p k = 851 fun decomp p k =
834 | Cond x => k [ACond x] 863 | Cond x => k [ACond x]
835 in 864 in
836 decomp 865 decomp
837 end 866 end
838 867
839 fun imply (p1, p2) = 868 fun imply (hyps, goals, outs) =
840 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 869 let
841 (fn hyps => 870 fun gls goals onFail acc =
842 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 871 case goals of
843 (fn goals => 872 [] =>
844 let 873 (let
845 fun gls goals onFail acc = 874 val cc = Cc.database ()
846 case goals of 875 val () = app (fn a => Cc.assert (cc, a)) hyps
847 [] => 876 in
848 (let 877 (List.all (fn a =>
849 val cc = Cc.database () 878 if Cc.check (cc, a) then
850 val () = app (fn a => Cc.assert (cc, a)) hyps 879 true
851 in 880 else
852 (List.all (fn a => 881 ((*Print.prefaces "Can't prove"
853 if Cc.check (cc, a) then 882 [("a", p_atom a),
854 true 883 ("hyps", Print.p_list p_atom hyps),
855 else 884 ("db", Cc.p_database cc)];*)
856 ((*Print.prefaces "Can't prove" 885 false)) acc
857 [("a", p_atom a), 886 (*andalso (Print.preface ("Finding", Cc.p_database cc); true)*)
858 ("hyps", Print.p_list p_atom hyps), 887 andalso Cc.builtFrom (cc, {Derived = Var 0,
859 ("db", Cc.p_database cc)];*) 888 Base = outs}))
860 false)) acc) 889 handle Cc.Contradiction => false
861 handle Cc.Contradiction => false 890 end handle Cc.Undetermined => false)
862 end handle Cc.Undetermined => false) 891 orelse onFail ()
863 orelse onFail () 892 | (g as AReln (Sql gf, [ge])) :: goals =>
864 | (g as AReln (Sql gf, [ge])) :: goals => 893 let
865 let 894 fun hps hyps =
866 fun hps hyps = 895 case hyps of
867 case hyps of 896 [] => gls goals onFail (g :: acc)
868 [] => gls goals onFail (g :: acc) 897 | (h as AReln (Sql hf, [he])) :: hyps =>
869 | (h as AReln (Sql hf, [he])) :: hyps => 898 if gf = hf then
870 if gf = hf then 899 let
871 let 900 val saved = save ()
872 val saved = save () 901 in
873 in 902 if eq (ge, he) then
874 if eq (ge, he) then 903 let
875 let 904 val changed = IM.numItems (!unif)
876 val changed = IM.numItems (!unif) 905 <> IM.numItems saved
877 <> IM.numItems saved 906 in
878 in 907 gls goals (fn () => (restore saved;
879 gls goals (fn () => (restore saved; 908 changed
880 changed 909 andalso hps hyps))
881 andalso hps hyps)) 910 acc
882 acc 911 end
883 end 912 else
884 else 913 hps hyps
885 hps hyps 914 end
886 end 915 else
887 else 916 hps hyps
888 hps hyps 917 | _ :: hyps => hps hyps
889 | _ :: hyps => hps hyps 918 in
890 in 919 hps hyps
891 hps hyps 920 end
892 end 921 | g :: goals => gls goals onFail (g :: acc)
893 | g :: goals => gls goals onFail (g :: acc) 922 in
894 in 923 reset ();
895 reset (); 924 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
896 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps), 925 ("goals", Print.p_list p_atom goals)];*)
897 ("goals", Print.p_list p_atom goals)];*) 926 gls goals (fn () => false) []
898 gls goals (fn () => false) [] 927 end handle Cc.Contradiction => true
899 end handle Cc.Contradiction => true))
900 928
901 fun patCon pc = 929 fun patCon pc =
902 case pc of 930 case pc of
903 PConVar n => "C" ^ Int.toString n 931 PConVar n => "C" ^ Int.toString n
904 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 932 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
1202 else 1230 else
1203 x :: ls 1231 x :: ls
1204 end 1232 end
1205 1233
1206 datatype queryMode = 1234 datatype queryMode =
1207 SomeCol of exp 1235 SomeCol
1208 | AllCols of exp 1236 | AllCols of exp
1209 1237
1210 exception Default 1238 exception Default
1211 1239
1212 fun queryProp env rvN rv oe e = 1240 fun queryProp env rvN rv oe e =
1213 let 1241 let
1214 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1242 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1215 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1243 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1216 (rvN, Unknown, Unknown, [])) 1244 (rvN, Unknown, Unknown, [], []))
1217 in 1245 in
1218 case parse query e of 1246 case parse query e of
1219 NONE => default () 1247 NONE => default ()
1220 | SOME r => 1248 | SOME r =>
1221 let 1249 let
1279 case expIn e of 1307 case expIn e of
1280 inr p' => And (p, p') 1308 inr p' => And (p, p')
1281 | _ => p 1309 | _ => p
1282 1310
1283 fun normal () = 1311 fun normal () =
1284 (And (p, case oe of 1312 case oe of
1285 SomeCol oe => 1313 SomeCol =>
1286 foldl (fn (si, p) => 1314 (rvN, p, True,
1287 let 1315 List.mapPartial (fn si =>
1288 val p' = case si of 1316 case si of
1289 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)]) 1317 SqField (v, f) => SOME (Proj (rvOf v, f))
1290 | SqExp (e, f) => 1318 | SqExp (e, f) =>
1291 case expIn e of 1319 case expIn e of
1292 inr _ => Unknown 1320 inr _ => NONE
1293 | inl e => Reln (Eq, [oe, e]) 1321 | inl e => SOME e) (#Select r))
1294 in 1322 | AllCols oe =>
1295 Or (p, p') 1323 (rvN, And (p, foldl (fn (si, p) =>
1296 end) 1324 let
1297 False (#Select r) 1325 val p' = case si of
1298 | AllCols oe => 1326 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
1299 foldl (fn (si, p) => 1327 Proj (rvOf v, f)])
1300 let 1328 | SqExp (e, f) =>
1301 val p' = case si of 1329 case expIn e of
1302 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f), 1330 inr p => Cond (Proj (oe, f), p)
1303 Proj (rvOf v, f)]) 1331 | inl e => Reln (Eq, [Proj (oe, f), e])
1304 | SqExp (e, f) => 1332 in
1305 case expIn e of
1306 inr p => Cond (Proj (oe, f), p)
1307 | inl e => Reln (Eq, [Proj (oe, f), e])
1308 in
1309 And (p, p') 1333 And (p, p')
1310 end) 1334 end)
1311 True (#Select r)), 1335 True (#Select r)),
1312 True) 1336 True, [])
1313 1337
1314 val (p, wp) = 1338 val (rvN, p, wp, outs) =
1315 case #Select r of 1339 case #Select r of
1316 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => 1340 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1317 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of 1341 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1318 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => 1342 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1319 let 1343 (case oe of
1320 val oe = case oe of 1344 SomeCol =>
1321 SomeCol oe => oe 1345 let
1322 | AllCols oe => Proj (oe, f) 1346 val (rvN, oe) = rv rvN
1323 in 1347 in
1324 (Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]), 1348 (rvN,
1325 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), 1349 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
1326 p)), 1350 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1327 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])])) 1351 p)),
1328 end 1352 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1353 [oe])
1354 end
1355 | AllCols oe =>
1356 let
1357 val oe = Proj (oe, f)
1358 in
1359 (rvN,
1360 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
1361 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1362 p)),
1363 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1364 [])
1365 end)
1329 | _ => normal ()) 1366 | _ => normal ())
1330 | _ => normal () 1367 | _ => normal ()
1331 in 1368 in
1332 (rvN, p, wp, case #Where r of 1369 (rvN, p, wp, case #Where r of
1333 NONE => [] 1370 NONE => []
1334 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)) 1371 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e), outs)
1335 end 1372 end
1336 handle Default => default () 1373 handle Default => default ()
1337 end 1374 end
1338 1375
1339 fun evalPat env e (pt, _) = 1376 fun evalPat env e (pt, _) =
1386 | _ => p2 1423 | _ => p2
1387 in 1424 in
1388 rr 1425 rr
1389 end 1426 end
1390 1427
1428 datatype cflow = Case | Where
1429 datatype flow = Data | Control of cflow
1430 type check = ErrorMsg.span * exp * prop
1431
1391 structure St :> sig 1432 structure St :> sig
1392 type t 1433 type t
1393 val create : {Var : int, 1434 val create : {Var : int,
1394 Ambient : prop} -> t 1435 Ambient : prop} -> t
1395 1436
1397 val nextVar : t -> t * int 1438 val nextVar : t -> t * int
1398 1439
1399 val ambient : t -> prop 1440 val ambient : t -> prop
1400 val setAmbient : t * prop -> t 1441 val setAmbient : t * prop -> t
1401 1442
1402 type check = ErrorMsg.span * exp * prop 1443 val paths : t -> (check * cflow) list
1403 1444 val addPath : t * (check * cflow) -> t
1404 val path : t -> check list 1445 val addPaths : t * (check * cflow) list -> t
1405 val addPath : t * check -> t 1446 val clearPaths : t -> t
1406 1447 val setPaths : t * (check * cflow) list -> t
1407 val sent : t -> check list 1448
1408 val addSent : t * check -> t 1449 val sent : t -> (check * flow) list
1409 val setSent : t * check list -> t 1450 val addSent : t * (check * flow) -> t
1451 val setSent : t * (check * flow) list -> t
1410 end = struct 1452 end = struct
1411
1412 type check = ErrorMsg.span * exp * prop
1413 1453
1414 type t = {Var : int, 1454 type t = {Var : int,
1415 Ambient : prop, 1455 Ambient : prop,
1416 Path : check list, 1456 Path : (check * cflow) list,
1417 Sent : check list} 1457 Sent : (check * flow) list}
1418 1458
1419 fun create {Var = v, Ambient = p} = {Var = v, 1459 fun create {Var = v, Ambient = p} = {Var = v,
1420 Ambient = p, 1460 Ambient = p,
1421 Path = [], 1461 Path = [],
1422 Sent = []} 1462 Sent = []}
1431 fun setAmbient (t : t, p) = {Var = #Var t, 1471 fun setAmbient (t : t, p) = {Var = #Var t,
1432 Ambient = p, 1472 Ambient = p,
1433 Path = #Path t, 1473 Path = #Path t,
1434 Sent = #Sent t} 1474 Sent = #Sent t}
1435 1475
1436 fun path (t : t) = #Path t 1476 fun paths (t : t) = #Path t
1437 fun addPath (t : t, c) = {Var = #Var t, 1477 fun addPath (t : t, c) = {Var = #Var t,
1438 Ambient = #Ambient t, 1478 Ambient = #Ambient t,
1439 Path = c :: #Path t, 1479 Path = c :: #Path t,
1440 Sent = #Sent t} 1480 Sent = #Sent t}
1481 fun addPaths (t : t, cs) = {Var = #Var t,
1482 Ambient = #Ambient t,
1483 Path = cs @ #Path t,
1484 Sent = #Sent t}
1485 fun clearPaths (t : t) = {Var = #Var t,
1486 Ambient = #Ambient t,
1487 Path = [],
1488 Sent = #Sent t}
1489 fun setPaths (t : t, cs) = {Var = #Var t,
1490 Ambient = #Ambient t,
1491 Path = cs,
1492 Sent = #Sent t}
1441 1493
1442 fun sent (t : t) = #Sent t 1494 fun sent (t : t) = #Sent t
1443 fun addSent (t : t, c) = {Var = #Var t, 1495 fun addSent (t : t, c) = {Var = #Var t,
1444 Ambient = #Ambient t, 1496 Ambient = #Ambient t,
1445 Path = #Path t, 1497 Path = #Path t,
1459 in 1511 in
1460 (Var nv, st) 1512 (Var nv, st)
1461 end 1513 end
1462 1514
1463 fun addSent (p, e, st) = 1515 fun addSent (p, e, st) =
1464 if isKnown e then 1516 let
1465 st 1517 val st = if isKnown e then
1466 else 1518 st
1467 St.addSent (st, (loc, e, p)) 1519 else
1520 St.addSent (st, ((loc, e, p), Data))
1521
1522 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
1523 in
1524 St.clearPaths st
1525 end
1468 in 1526 in
1469 case #1 e of 1527 case #1 e of
1470 EPrim p => (Const p, st) 1528 EPrim p => (Const p, st)
1471 | ERel n => (List.nth (env, n), st) 1529 | ERel n => (List.nth (env, n), st)
1472 | ENamed _ => default () 1530 | ENamed _ => default ()
1540 let 1598 let
1541 val (e, st) = evalExp env (e, st) 1599 val (e, st) = evalExp env (e, st)
1542 in 1600 in
1543 (Proj (e, s), st) 1601 (Proj (e, s), st)
1544 end 1602 end
1545 | ECase (e, pes, _) => 1603 | ECase (e, pes, {result = res, ...}) =>
1546 let 1604 let
1547 val (e, st) = evalExp env (e, st) 1605 val (e, st) = evalExp env (e, st)
1548 val (st, r) = St.nextVar st 1606 val (st, r) = St.nextVar st
1549 val orig = St.ambient st 1607 val orig = St.ambient st
1550 1608 val origPaths = St.paths st
1551 val st = foldl (fn ((pt, pe), st) => 1609
1552 let 1610 val st = St.addPath (st, ((loc, e, orig), Case))
1553 val (env, pp) = evalPat env e pt 1611
1554 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp))) 1612 val (st, paths) =
1555 (*val () = Print.prefaces "Case" [("loc", Print.PD.string 1613 foldl (fn ((pt, pe), (st, paths)) =>
1556 (ErrorMsg.spanToString (#2 pt))), 1614 let
1557 ("env", Print.p_list p_exp env), 1615 val (env, pp) = evalPat env e pt
1558 ("sent", Print.p_list_sep Print.PD.newline 1616 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
1559 (fn (loc, e, p) => 1617
1560 Print.box [Print.PD.string 1618 val this = And (removeRedundant orig (St.ambient st'),
1561 (ErrorMsg.spanToString loc), 1619 Reln (Eq, [Var r, pe]))
1562 Print.PD.string ":", 1620 in
1563 Print.space, 1621 (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths),
1564 p_exp e, 1622 St.paths st' @ paths)
1565 Print.space, 1623 end) (St.setAmbient (st, False), []) pes
1566 Print.PD.string "in", 1624
1567 Print.space, 1625 val st = case #1 res of
1568 p_prop p]) 1626 TRecord [] => St.setPaths (st, origPaths)
1569 (List.take (#3 st', length (#3 st') 1627 | _ => St.setPaths (st, paths)
1570 - length (#3 st))))]*)
1571
1572 val this = And (removeRedundant orig (St.ambient st'),
1573 Reln (Eq, [Var r, pe]))
1574 in
1575 St.setAmbient (st', Or (St.ambient st, this))
1576 end) (St.setAmbient (st, False)) pes
1577 in 1628 in
1578 (Var r, St.setAmbient (st, And (orig, St.ambient st))) 1629 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
1579 end 1630 end
1580 | EStrcat (e1, e2) => 1631 | EStrcat (e1, e2) =>
1581 let 1632 let
1631 val (st', r) = St.nextVar st 1682 val (st', r) = St.nextVar st
1632 val (st', acc) = St.nextVar st' 1683 val (st', acc) = St.nextVar st'
1633 1684
1634 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1685 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
1635 1686
1636 val (st', qp, qwp, used) = 1687 val (st', qp, qwp, used, _) =
1637 queryProp env 1688 queryProp env
1638 st' (fn st' => 1689 st' (fn st' =>
1639 let 1690 let
1640 val (st', rv) = St.nextVar st' 1691 val (st', rv) = St.nextVar st'
1641 in 1692 in
1660 p')) 1711 p'))
1661 in 1712 in
1662 (St.setAmbient (st, p), Var out) 1713 (St.setAmbient (st, p), Var out)
1663 end 1714 end
1664 1715
1665 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (St.sent st') 1716 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
1666 1717
1667 val p' = And (p', qwp) 1718 val p' = And (p', qwp)
1668 val sent = map (fn e => (loc, e, p')) used @ sent 1719 val paths = map (fn e => ((loc, e, p'), Where)) used
1669 in 1720 in
1670 (res, St.setSent (st, sent)) 1721 (res, St.addPaths (St.setSent (st, sent), paths))
1671 end 1722 end
1672 | EDml _ => default () 1723 | EDml _ => default ()
1673 | ENextval _ => default () 1724 | ENextval _ => default ()
1674 | ESetval _ => default () 1725 | ESetval _ => default ()
1675 1726
1726 Ambient = p}) 1777 Ambient = p})
1727 in 1778 in
1728 (St.sent st @ vals, pols) 1779 (St.sent st @ vals, pols)
1729 end 1780 end
1730 1781
1731 | DPolicy (PolClient e) => (vals, #2 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN)) 1782 | DPolicy (PolClient e) =>
1732 (SomeCol (Var 0)) e) :: pols) 1783 let
1784 val (_, p, _, _, outs) = queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN)) SomeCol e
1785 in
1786 (vals, (p, outs) :: pols)
1787 end
1733 1788
1734 | _ => (vals, pols) 1789 | _ => (vals, pols)
1735 1790
1736 val () = reset () 1791 val () = reset ()
1737 1792
1738 val (vals, pols) = foldl decl ([], []) file 1793 val (vals, pols) = foldl decl ([], []) file
1739 in 1794 in
1740 app (fn (loc, e, p) => 1795 app (fn ((loc, e, p), fl) =>
1741 let 1796 let
1742 fun doOne e = 1797 fun doOne e =
1743 let 1798 let
1744 val p = And (p, Reln (Eq, [Var 0, e])) 1799 val p = And (p, Reln (Eq, [Var 0, e]))
1745 in 1800 in
1746 if List.exists (fn pol => if imply (p, pol) then 1801 if decomp true (fn (e1, e2) => e1 andalso e2 ()) p
1747 (if !debug then 1802 (fn hyps =>
1748 Print.prefaces "Match" 1803 (fl <> Control Where
1749 [("Hyp", p_prop p), 1804 andalso imply (hyps, [AReln (Known, [Var 0])], [Var 0]))
1750 ("Goal", p_prop pol)] 1805 orelse List.exists (fn (p', outs) =>
1751 else 1806 decomp false (fn (e1, e2) => e1 orelse e2 ()) p'
1752 (); 1807 (fn goals => imply (hyps, goals, outs)))
1753 true) 1808 pols) then
1754 else
1755 false) pols then
1756 () 1809 ()
1757 else 1810 else
1758 (ErrorMsg.errorAt loc "The information flow policy may be violated here."; 1811 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1759 Print.preface ("The state satisifies this predicate:", p_prop p)) 1812 Print.preface ("The state satisifies this predicate:", p_prop p))
1760 end 1813 end