Mercurial > urweb

comparison src/iflow.sml @ 1217:4d206e603300

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Abstract type for evalExp state; handle WHERE conditions soundly
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 10:24:13 -0400
parents 09caa8c780e5
children 48d2ca496d2c
comparison
equal deleted inserted replaced
1216:09caa8c780e5 1217:4d206e603300
835 in 835 in
836 decomp 836 decomp
837 end 837 end
838 838
839 fun imply (p1, p2) = 839 fun imply (p1, p2) =
840 (reset (); 840 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
841 (*Print.prefaces "Bigger go" [("p1", p_prop p1), 841 (fn hyps =>
842 ("p2", p_prop p2)];*) 842 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
843 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1 843 (fn goals =>
844 (fn hyps => 844 let
845 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2 845 fun gls goals onFail acc =
846 (fn goals => 846 case goals of
847 let 847 [] =>
848 fun gls goals onFail acc = 848 (let
849 case goals of 849 val cc = Cc.database ()
850 [] => 850 val () = app (fn a => Cc.assert (cc, a)) hyps
851 (let 851 in
852 val cc = Cc.database () 852 (List.all (fn a =>
853 val () = app (fn a => Cc.assert (cc, a)) hyps 853 if Cc.check (cc, a) then
854 in 854 true
855 (List.all (fn a => 855 else
856 if Cc.check (cc, a) then 856 ((*Print.prefaces "Can't prove"
857 true 857 [("a", p_atom a),
858 ("hyps", Print.p_list p_atom hyps),
859 ("db", Cc.p_database cc)];*)
860 false)) acc)
861 handle Cc.Contradiction => false
862 end handle Cc.Undetermined => false)
863 orelse onFail ()
864 | (g as AReln (Sql gf, [ge])) :: goals =>
865 let
866 fun hps hyps =
867 case hyps of
868 [] => gls goals onFail (g :: acc)
869 | (h as AReln (Sql hf, [he])) :: hyps =>
870 if gf = hf then
871 let
872 val saved = save ()
873 in
874 if eq (ge, he) then
875 let
876 val changed = IM.numItems (!unif)
877 <> IM.numItems saved
878 in
879 gls goals (fn () => (restore saved;
880 changed
881 andalso hps hyps))
882 acc
883 end
858 else 884 else
859 ((*Print.prefaces "Can't prove" 885 hps hyps
860 [("a", p_atom a), 886 end
861 ("hyps", Print.p_list p_atom hyps), 887 else
862 ("db", Cc.p_database cc)];*) 888 hps hyps
863 false)) acc 889 | _ :: hyps => hps hyps
864 orelse onFail ()) 890 in
865 handle Cc.Contradiction => onFail () 891 hps hyps
866 end handle Cc.Undetermined => ((*print "Undetermined\n";*) onFail ())) 892 end
867 | (g as AReln (Sql gf, [ge])) :: goals => 893 | g :: goals => gls goals onFail (g :: acc)
868 let 894 in
869 fun hps hyps = 895 reset ();
870 case hyps of 896 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
871 [] => gls goals onFail (g :: acc) 897 ("goals", Print.p_list p_atom goals)];*)
872 | AReln (Sql hf, [he]) :: hyps => 898 gls goals (fn () => false) []
873 if gf = hf then 899 end handle Cc.Contradiction => true))
874 let
875 val saved = save ()
876 in
877 if eq (ge, he) then
878 let
879 val changed = IM.numItems (!unif)
880 <> IM.numItems saved
881 in
882 gls goals (fn () => (restore saved;
883 changed
884 andalso hps hyps))
885 acc
886 end
887 else
888 hps hyps
889 end
890 else
891 hps hyps
892 | _ :: hyps => hps hyps
893 in
894 hps hyps
895 end
896 | g :: goals => gls goals onFail (g :: acc)
897 in
898 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
899 ("goals", Print.p_list p_atom goals)];*)
900 gls goals (fn () => false) []
901 end handle Cc.Contradiction => true)))
902 900
903 fun patCon pc = 901 fun patCon pc =
904 case pc of 902 case pc of
905 PConVar n => "C" ^ Int.toString n 903 PConVar n => "C" ^ Int.toString n
906 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c 904 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
1213 1211
1214 fun queryProp env rvN rv oe e = 1212 fun queryProp env rvN rv oe e =
1215 let 1213 let
1216 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1214 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1217 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1215 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1218 (rvN, Unknown, [])) 1216 (rvN, Unknown, Unknown, []))
1219 in 1217 in
1220 case parse query e of 1218 case parse query e of
1221 NONE => default () 1219 NONE => default ()
1222 | SOME r => 1220 | SOME r =>
1223 let 1221 let
1281 case expIn e of 1279 case expIn e of
1282 inr p' => And (p, p') 1280 inr p' => And (p, p')
1283 | _ => p 1281 | _ => p
1284 1282
1285 fun normal () = 1283 fun normal () =
1286 (rvN, 1284 (And (p, case oe of
1287 And (p, case oe of
1288 SomeCol oe => 1285 SomeCol oe =>
1289 foldl (fn (si, p) => 1286 foldl (fn (si, p) =>
1290 let 1287 let
1291 val p' = case si of 1288 val p' = case si of
1292 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)]) 1289 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
1310 | inl e => Reln (Eq, [Proj (oe, f), e]) 1307 | inl e => Reln (Eq, [Proj (oe, f), e])
1311 in 1308 in
1312 And (p, p') 1309 And (p, p')
1313 end) 1310 end)
1314 True (#Select r)), 1311 True (#Select r)),
1315 case #Where r of 1312 True)
1316 NONE => [] 1313
1317 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)) 1314 val (p, wp) =
1318 in 1315 case #Select r of
1319 case #Select r of 1316 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1320 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] => 1317 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1321 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of 1318 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1322 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) => 1319 let
1323 let 1320 val oe = case oe of
1324 val oe = case oe of 1321 SomeCol oe => oe
1325 SomeCol oe => oe 1322 | AllCols oe => Proj (oe, f)
1326 | AllCols oe => Proj (oe, f) 1323 in
1327 in 1324 (Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
1328 (rvN, 1325 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1329 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]), 1326 p)),
1330 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]), 1327 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]))
1331 p)), 1328 end
1332 []) 1329 | _ => normal ())
1333 end 1330 | _ => normal ()
1334 | _ => normal ()) 1331 in
1335 | _ => normal () 1332 (rvN, p, wp, case #Where r of
1333 NONE => []
1334 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
1336 end 1335 end
1337 handle Default => default () 1336 handle Default => default ()
1338 end 1337 end
1339 1338
1340 fun evalPat env e (pt, _) = 1339 fun evalPat env e (pt, _) =
1387 | _ => p2 1386 | _ => p2
1388 in 1387 in
1389 rr 1388 rr
1390 end 1389 end
1391 1390
1392 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = 1391 structure St :> sig
1392 type t
1393 val create : {Var : int,
1394 Ambient : prop} -> t
1395
1396 val curVar : t -> int
1397 val nextVar : t -> t * int
1398
1399 val ambient : t -> prop
1400 val setAmbient : t * prop -> t
1401
1402 type check = ErrorMsg.span * exp * prop
1403
1404 val path : t -> check list
1405 val addPath : t * check -> t
1406
1407 val sent : t -> check list
1408 val addSent : t * check -> t
1409 val setSent : t * check list -> t
1410 end = struct
1411
1412 type check = ErrorMsg.span * exp * prop
1413
1414 type t = {Var : int,
1415 Ambient : prop,
1416 Path : check list,
1417 Sent : check list}
1418
1419 fun create {Var = v, Ambient = p} = {Var = v,
1420 Ambient = p,
1421 Path = [],
1422 Sent = []}
1423
1424 fun curVar (t : t) = #Var t
1425 fun nextVar (t : t) = ({Var = #Var t + 1,
1426 Ambient = #Ambient t,
1427 Path = #Path t,
1428 Sent = #Sent t}, #Var t)
1429
1430 fun ambient (t : t) = #Ambient t
1431 fun setAmbient (t : t, p) = {Var = #Var t,
1432 Ambient = p,
1433 Path = #Path t,
1434 Sent = #Sent t}
1435
1436 fun path (t : t) = #Path t
1437 fun addPath (t : t, c) = {Var = #Var t,
1438 Ambient = #Ambient t,
1439 Path = c :: #Path t,
1440 Sent = #Sent t}
1441
1442 fun sent (t : t) = #Sent t
1443 fun addSent (t : t, c) = {Var = #Var t,
1444 Ambient = #Ambient t,
1445 Path = #Path t,
1446 Sent = c :: #Sent t}
1447 fun setSent (t : t, cs) = {Var = #Var t,
1448 Ambient = #Ambient t,
1449 Path = #Path t,
1450 Sent = cs}
1451
1452 end
1453
1454 fun evalExp env (e as (_, loc), st) =
1393 let 1455 let
1394 fun default () = 1456 fun default () =
1395 ((*Print.preface ("Default" ^ Int.toString nv, 1457 let
1396 MonoPrint.p_exp MonoEnv.empty e);*) 1458 val (st, nv) = St.nextVar st
1397 (Var nv, (nv+1, p, sent))) 1459 in
1398 1460 (Var nv, st)
1399 fun addSent (p, e, sent) = 1461 end
1462
1463 fun addSent (p, e, st) =
1400 if isKnown e then 1464 if isKnown e then
1401 sent 1465 st
1402 else 1466 else
1403 (loc, e, p) :: sent 1467 St.addSent (st, (loc, e, p))
1404 in 1468 in
1405 case #1 e of 1469 case #1 e of
1406 EPrim p => (Const p, st) 1470 EPrim p => (Const p, st)
1407 | ERel n => (List.nth (env, n), st) 1471 | ERel n => (List.nth (env, n), st)
1408 | ENamed _ => default () 1472 | ENamed _ => default ()
1425 | EFfiApp (m, s, es) => 1489 | EFfiApp (m, s, es) =>
1426 if m = "Basis" andalso SS.member (writers, s) then 1490 if m = "Basis" andalso SS.member (writers, s) then
1427 let 1491 let
1428 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1492 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1429 in 1493 in
1430 (Recd [], (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es)) 1494 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
1431 end 1495 end
1432 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then 1496 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
1433 default () 1497 default ()
1434 else 1498 else
1435 let 1499 let
1479 (Proj (e, s), st) 1543 (Proj (e, s), st)
1480 end 1544 end
1481 | ECase (e, pes, _) => 1545 | ECase (e, pes, _) =>
1482 let 1546 let
1483 val (e, st) = evalExp env (e, st) 1547 val (e, st) = evalExp env (e, st)
1484 val r = #1 st 1548 val (st, r) = St.nextVar st
1485 val st = (r + 1, #2 st, #3 st) 1549 val orig = St.ambient st
1486 val orig = #2 st
1487 1550
1488 val st = foldl (fn ((pt, pe), st) => 1551 val st = foldl (fn ((pt, pe), st) =>
1489 let 1552 let
1490 val (env, pp) = evalPat env e pt 1553 val (env, pp) = evalPat env e pt
1491 val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st)) 1554 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
1492 (*val () = Print.prefaces "Case" [("loc", Print.PD.string 1555 (*val () = Print.prefaces "Case" [("loc", Print.PD.string
1493 (ErrorMsg.spanToString (#2 pt))), 1556 (ErrorMsg.spanToString (#2 pt))),
1494 ("env", Print.p_list p_exp env), 1557 ("env", Print.p_list p_exp env),
1495 ("sent", Print.p_list_sep Print.PD.newline 1558 ("sent", Print.p_list_sep Print.PD.newline
1496 (fn (loc, e, p) => 1559 (fn (loc, e, p) =>
1504 Print.space, 1567 Print.space,
1505 p_prop p]) 1568 p_prop p])
1506 (List.take (#3 st', length (#3 st') 1569 (List.take (#3 st', length (#3 st')
1507 - length (#3 st))))]*) 1570 - length (#3 st))))]*)
1508 1571
1509 val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe])) 1572 val this = And (removeRedundant orig (St.ambient st'),
1573 Reln (Eq, [Var r, pe]))
1510 in 1574 in
1511 (#1 st', Or (#2 st, this), #3 st') 1575 St.setAmbient (st', Or (St.ambient st, this))
1512 end) (#1 st, False, #3 st) pes 1576 end) (St.setAmbient (st, False)) pes
1513 in 1577 in
1514 (Var r, (#1 st, And (orig, #2 st), #3 st)) 1578 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
1515 end 1579 end
1516 | EStrcat (e1, e2) => 1580 | EStrcat (e1, e2) =>
1517 let 1581 let
1518 val (e1, st) = evalExp env (e1, st) 1582 val (e1, st) = evalExp env (e1, st)
1519 val (e2, st) = evalExp env (e2, st) 1583 val (e2, st) = evalExp env (e2, st)
1524 | EReturnBlob {blob = b, mimeType = m, ...} => 1588 | EReturnBlob {blob = b, mimeType = m, ...} =>
1525 let 1589 let
1526 val (b, st) = evalExp env (b, st) 1590 val (b, st) = evalExp env (b, st)
1527 val (m, st) = evalExp env (m, st) 1591 val (m, st) = evalExp env (m, st)
1528 in 1592 in
1529 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent)))) 1593 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
1530 end 1594 end
1531 | ERedirect (e, _) => 1595 | ERedirect (e, _) =>
1532 let 1596 let
1533 val (e, st) = evalExp env (e, st) 1597 val (e, st) = evalExp env (e, st)
1534 in 1598 in
1535 (Finish, (#1 st, p, addSent (#2 st, e, sent))) 1599 (Finish, addSent (St.ambient st, e, st))
1536 end 1600 end
1537 | EWrite e => 1601 | EWrite e =>
1538 let 1602 let
1539 val (e, st) = evalExp env (e, st) 1603 val (e, st) = evalExp env (e, st)
1540 in 1604 in
1541 (Recd [], (#1 st, p, addSent (#2 st, e, sent))) 1605 (Recd [], addSent (St.ambient st, e, st))
1542 end 1606 end
1543 | ESeq (e1, e2) => 1607 | ESeq (e1, e2) =>
1544 let 1608 let
1545 val (_, st) = evalExp env (e1, st) 1609 val (_, st) = evalExp env (e1, st)
1546 in 1610 in
1562 | EQuery {query = q, body = b, initial = i, ...} => 1626 | EQuery {query = q, body = b, initial = i, ...} =>
1563 let 1627 let
1564 val (_, st) = evalExp env (q, st) 1628 val (_, st) = evalExp env (q, st)
1565 val (i, st) = evalExp env (i, st) 1629 val (i, st) = evalExp env (i, st)
1566 1630
1567 val r = #1 st 1631 val (st', r) = St.nextVar st
1568 val acc = #1 st + 1 1632 val (st', acc) = St.nextVar st'
1569 val st' = (#1 st + 2, #2 st, #3 st)
1570 1633
1571 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 1634 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
1572 1635
1573 val (rvN, qp, used) = 1636 val (st', qp, qwp, used) =
1574 queryProp env 1637 queryProp env
1575 (#1 st') (fn rvN => (rvN + 1, Var rvN)) 1638 st' (fn st' =>
1639 let
1640 val (st', rv) = St.nextVar st'
1641 in
1642 (st', Var rv)
1643 end)
1576 (AllCols (Var r)) q 1644 (AllCols (Var r)) q
1577 1645
1578 val p' = And (qp, #2 st') 1646 val p' = And (qp, St.ambient st')
1579 1647
1580 val (nvs, p, res) = if varInP acc (#2 st') then 1648 val (st, res) = if varInP acc (St.ambient st') then
1581 (#1 st + 1, #2 st, Var r) 1649 let
1582 else 1650 val (st, r) = St.nextVar st
1583 let 1651 in
1584 val out = rvN 1652 (st, Var r)
1585 1653 end
1586 val p = Or (Reln (Eq, [Var out, i]), 1654 else
1587 And (Reln (Eq, [Var out, b]), 1655 let
1588 p')) 1656 val (st, out) = St.nextVar st'
1589 in 1657
1590 (out + 1, p, Var out) 1658 val p = Or (Reln (Eq, [Var out, i]),
1591 end 1659 And (Reln (Eq, [Var out, b]),
1592 1660 p'))
1593 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (#3 st') 1661 in
1662 (St.setAmbient (st, p), Var out)
1663 end
1664
1665 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (St.sent st')
1666
1667 val p' = And (p', qwp)
1594 val sent = map (fn e => (loc, e, p')) used @ sent 1668 val sent = map (fn e => (loc, e, p')) used @ sent
1595 in 1669 in
1596 (res, (nvs, p, sent)) 1670 (res, St.setSent (st, sent))
1597 end 1671 end
1598 | EDml _ => default () 1672 | EDml _ => default ()
1599 | ENextval _ => default () 1673 | ENextval _ => default ()
1600 | ESetval _ => default () 1674 | ESetval _ => default ()
1601 1675
1602 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) => 1676 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
1603 (Var nv, (nv + 1, And (p, Reln (Known, [Var nv])), sent)) 1677 let
1678 val (st, nv) = St.nextVar st
1679 in
1680 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
1681 end
1604 1682
1605 | EUnurlify _ => default () 1683 | EUnurlify _ => default ()
1606 | EJavaScript _ => default () 1684 | EJavaScript _ => default ()
1607 | ESignalReturn _ => default () 1685 | ESignalReturn _ => default ()
1608 | ESignalBind _ => default () 1686 | ESignalBind _ => default ()
1642 p) 1720 p)
1643 | _ => (e, env, nv, p) 1721 | _ => (e, env, nv, p)
1644 1722
1645 val (e, env, nv, p) = deAbs (e, [], 1, True) 1723 val (e, env, nv, p) = deAbs (e, [], 1, True)
1646 1724
1647 val (e, (_, p, sent)) = evalExp env (e, (nv, p, [])) 1725 val (_, st) = evalExp env (e, St.create {Var = nv,
1726 Ambient = p})
1648 in 1727 in
1649 (sent @ vals, pols) 1728 (St.sent st @ vals, pols)
1650 end 1729 end
1651 1730
1652 | DPolicy (PolClient e) => (vals, #2 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN)) 1731 | DPolicy (PolClient e) => (vals, #2 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
1653 (SomeCol (Var 0)) e) :: pols) 1732 (SomeCol (Var 0)) e) :: pols)
1654 1733