Mercurial > urweb

comparison src/iflow.sml @ 1227:1d8fba74e7f5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Iflow working with a UNION
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 16:06:16 -0400
parents df5bd4115267
children 7dfa67560916
comparison
equal deleted inserted replaced
1226:df5bd4115267 1227:1d8fba74e7f5
967 ((*Print.prefaces "Can't prove" 967 ((*Print.prefaces "Can't prove"
968 [("a", p_atom a), 968 [("a", p_atom a),
969 ("hyps", Print.p_list p_atom hyps), 969 ("hyps", Print.p_list p_atom hyps),
970 ("db", Cc.p_database cc)];*) 970 ("db", Cc.p_database cc)];*)
971 false)) acc 971 false)) acc
972 (*andalso (Print.preface ("Finding", Cc.p_database cc); true)*) 972 andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true)
973 andalso (case outs of 973 andalso (case outs of
974 NONE => true 974 NONE => true
975 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0, 975 | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
976 Base = outs}))) 976 Base = outs})))
977 handle Cc.Contradiction => false 977 handle Cc.Contradiction => false
1127 fun ws p = wrap (follow (skip (fn ch => ch = #" ")) 1127 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
1128 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2) 1128 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
1129 1129
1130 fun log name p chs = 1130 fun log name p chs =
1131 (if !debug then 1131 (if !debug then
1132 case chs of 1132 (print (name ^ ": ");
1133 String s :: _ => print (name ^ ": " ^ s ^ "\n") 1133 app (fn String s => print s
1134 | _ => print (name ^ ": blocked!\n") 1134 | _ => print "???") chs;
1135 print "\n")
1135 else 1136 else
1136 (); 1137 ();
1137 p chs) 1138 p chs)
1138 1139
1139 fun list p chs = 1140 fun list p chs =
1300 (fn ((), ls) => ls)) 1301 (fn ((), ls) => ls))
1301 1302
1302 val wher = wrap (follow (ws (const "WHERE ")) sqexp) 1303 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
1303 (fn ((), ls) => ls) 1304 (fn ((), ls) => ls)
1304 1305
1305 val query = log "query" 1306 type query1 = {Select : sitem list,
1307 From : (string * string) list,
1308 Where : sqexp option}
1309
1310 val query1 = log "query1"
1306 (wrap (follow (follow select from) (opt wher)) 1311 (wrap (follow (follow select from) (opt wher))
1307 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})) 1312 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
1313
1314 datatype query =
1315 Query1 of query1
1316 | Union of query * query
1317
1318 fun query chs = log "query"
1319 (alt (wrap (follow (const "((")
1320 (follow query
1321 (follow (const ") UNION (")
1322 (follow query (const "))")))))
1323 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
1324 (wrap query1 Query1))
1325 chs
1308 1326
1309 datatype dml = 1327 datatype dml =
1310 Insert of string * (string * sqexp) list 1328 Insert of string * (string * sqexp) list
1311 | Delete of string * sqexp 1329 | Delete of string * sqexp
1312 | Update of string * (string * sqexp) list * sqexp 1330 | Update of string * (string * sqexp) list * sqexp
1429 1447
1430 fun queryProp env rvN rv oe e = 1448 fun queryProp env rvN rv oe e =
1431 let 1449 let
1432 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1450 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1433 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1451 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1434 (rvN, Unknown, Unknown, [], [])) 1452 (rvN, Unknown, [], []))
1435 in 1453 in
1436 case parse query e of 1454 case parse query e of
1437 NONE => default () 1455 NONE => default ()
1438 | SOME r => 1456 | SOME q =>
1439 let 1457 let
1440 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => 1458 fun doQuery (q, rvN) =
1441 let 1459 case q of
1442 val (rvN, e) = rv rvN 1460 Query1 r =>
1443 in
1444 ((v, e), rvN)
1445 end) rvN (#From r)
1446
1447 fun rvOf v =
1448 case List.find (fn (v', _) => v' = v) rvs of
1449 NONE => raise Fail "Iflow.queryProp: Bad table variable"
1450 | SOME (_, e) => e
1451
1452 fun usedFields e =
1453 case e of
1454 SqConst _ => []
1455 | Field (v, f) => [(v, f)]
1456 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
1457 | SqKnown _ => []
1458 | Inj _ => []
1459 | SqFunc (_, e) => usedFields e
1460 | Count => []
1461
1462 val p =
1463 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
1464
1465 val expIn = expIn rv env rvOf
1466
1467 val (p, rvN) = case #Where r of
1468 NONE => (p, rvN)
1469 | SOME e =>
1470 case expIn (e, rvN) of
1471 (inr p', rvN) => (And (p, p'), rvN)
1472 | _ => (p, rvN)
1473
1474 fun normal () =
1475 case oe of
1476 SomeCol =>
1477 let 1461 let
1478 val (sis, rvN) = 1462 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1479 ListUtil.foldlMap 1463 let
1480 (fn (si, rvN) => 1464 val (rvN, e) = rv rvN
1481 case si of 1465 in
1482 SqField (v, f) => (Proj (rvOf v, f), rvN) 1466 ((v, e), rvN)
1483 | SqExp (e, f) => 1467 end) rvN (#From r)
1484 case expIn (e, rvN) of 1468
1485 (inr _, _) => 1469 fun rvOf v =
1486 let 1470 case List.find (fn (v', _) => v' = v) rvs of
1487 val (rvN, e) = rv rvN 1471 NONE => raise Fail "Iflow.queryProp: Bad table variable"
1488 in 1472 | SOME (_, e) => e
1489 (e, rvN) 1473
1490 end 1474 fun usedFields e =
1491 | (inl e, rvN) => (e, rvN)) rvN (#Select r) 1475 case e of
1476 SqConst _ => []
1477 | Field (v, f) => [(v, f)]
1478 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
1479 | SqKnown _ => []
1480 | Inj _ => []
1481 | SqFunc (_, e) => usedFields e
1482 | Count => []
1483
1484 val p =
1485 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
1486
1487 val expIn = expIn rv env rvOf
1488
1489 val (p, rvN) = case #Where r of
1490 NONE => (p, rvN)
1491 | SOME e =>
1492 case expIn (e, rvN) of
1493 (inr p', rvN) => (And (p, p'), rvN)
1494 | _ => (p, rvN)
1495
1496 fun normal () =
1497 case oe of
1498 SomeCol =>
1499 let
1500 val (sis, rvN) =
1501 ListUtil.foldlMap
1502 (fn (si, rvN) =>
1503 case si of
1504 SqField (v, f) => (Proj (rvOf v, f), rvN)
1505 | SqExp (e, f) =>
1506 case expIn (e, rvN) of
1507 (inr _, _) =>
1508 let
1509 val (rvN, e) = rv rvN
1510 in
1511 (e, rvN)
1512 end
1513 | (inl e, rvN) => (e, rvN)) rvN (#Select r)
1514 in
1515 (rvN, p, True, sis)
1516 end
1517 | AllCols oe =>
1518 let
1519 val (ts, es, rvN) =
1520 foldl (fn (si, (ts, es, rvN)) =>
1521 case si of
1522 SqField (v, f) =>
1523 let
1524 val fs = getOpt (SM.find (ts, v), SM.empty)
1525 in
1526 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN)
1527 end
1528 | SqExp (e, f) =>
1529 let
1530 val (e, rvN) =
1531 case expIn (e, rvN) of
1532 (inr _, rvN) =>
1533 let
1534 val (rvN, e) = rv rvN
1535 in
1536 (e, rvN)
1537 end
1538 | (inl e, rvN) => (e, rvN)
1539 in
1540 (ts, SM.insert (es, f, e), rvN)
1541 end)
1542 (SM.empty, SM.empty, rvN) (#Select r)
1543
1544 val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
1545 (SM.listItemsi ts)
1546 @ SM.listItemsi es)])
1547 in
1548 (rvN, And (p, p'), True, [])
1549 end
1550
1551 val (rvN, p, wp, outs) =
1552 case #Select r of
1553 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1554 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1555 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1556 (case oe of
1557 SomeCol =>
1558 let
1559 val (rvN, oe) = rv rvN
1560 in
1561 (rvN,
1562 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
1563 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1564 p)),
1565 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1566 [oe])
1567 end
1568 | AllCols oe =>
1569 let
1570 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
1571 in
1572 (rvN,
1573 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
1574 And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
1575 p)),
1576 oeEq (Func (DtCon0 "Basis.bool.True", [])),
1577 [])
1578 end)
1579 | _ => normal ())
1580 | _ => normal ()
1492 in 1581 in
1493 (rvN, p, True, sis) 1582 (rvN, p, map (fn x => (wp, x))
1583 (case #Where r of
1584 NONE => []
1585 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)), outs)
1494 end 1586 end
1495 | AllCols oe => 1587 | Union (q1, q2) =>
1496 let 1588 let
1497 val (ts, es, rvN) = 1589 val (rvN, p1, used1, outs1) = doQuery (q1, rvN)
1498 foldl (fn (si, (ts, es, rvN)) => 1590 val (rvN, p2, used2, outs2) = doQuery (q2, rvN)
1499 case si of
1500 SqField (v, f) =>
1501 let
1502 val fs = getOpt (SM.find (ts, v), SM.empty)
1503 in
1504 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN)
1505 end
1506 | SqExp (e, f) =>
1507 let
1508 val (e, rvN) =
1509 case expIn (e, rvN) of
1510 (inr _, rvN) =>
1511 let
1512 val (rvN, e) = rv rvN
1513 in
1514 (e, rvN)
1515 end
1516 | (inl e, rvN) => (e, rvN)
1517 in
1518 (ts, SM.insert (es, f, e), rvN)
1519 end)
1520 (SM.empty, SM.empty, rvN) (#Select r)
1521
1522 val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
1523 (SM.listItemsi ts)
1524 @ SM.listItemsi es)])
1525 in 1591 in
1526 (rvN, And (p, p'), True, []) 1592 case (outs1, outs2) of
1593 ([], []) => (rvN, Or (p1, p2),
1594 map (fn (p, e) => (And (p1, p), e)) used1
1595 @ map (fn (p, e) => (And (p2, p), e)) used2, [])
1596 | _ => default ()
1527 end 1597 end
1528 1598 in
1529 val (rvN, p, wp, outs) = 1599 doQuery (q, rvN)
1530 case #Select r of
1531 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
1532 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
1533 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
1534 (case oe of
1535 SomeCol =>
1536 let
1537 val (rvN, oe) = rv rvN
1538 in
1539 (rvN,
1540 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
1541 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1542 p)),
1543 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
1544 [oe])
1545 end
1546 | AllCols oe =>
1547 let
1548 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
1549 in
1550 (rvN,
1551 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
1552 And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
1553 p)),
1554 oeEq (Func (DtCon0 "Basis.bool.True", [])),
1555 [])
1556 end)
1557 | _ => normal ())
1558 | _ => normal ()
1559 in
1560 (rvN, p, wp, case #Where r of
1561 NONE => []
1562 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e), outs)
1563 end 1600 end
1564 end 1601 end
1565 1602
1566 fun insertProp rvN rv e = 1603 fun insertProp rvN rv e =
1567 let 1604 let
1568 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1605 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1569 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1606 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1570 Unknown) 1607 Unknown)
1571 in 1608 in
1572 case parse query e of 1609 case parse query e of
1573 NONE => default () 1610 SOME (Query1 r) =>
1574 | SOME r =>
1575 let 1611 let
1576 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => 1612 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1577 let 1613 let
1578 val (rvN, e) = rv rvN 1614 val (rvN, e) = rv rvN
1579 in 1615 in
1603 | SOME e => 1639 | SOME e =>
1604 case expIn (e, rvN) of 1640 case expIn (e, rvN) of
1605 (inr p', _) => And (p, p') 1641 (inr p', _) => And (p, p')
1606 | _ => p 1642 | _ => p
1607 end 1643 end
1644 | _ => default ()
1608 end 1645 end
1609 1646
1610 fun deleteProp rvN rv e = 1647 fun deleteProp rvN rv e =
1611 let 1648 let
1612 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1649 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1613 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1650 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1614 Unknown) 1651 Unknown)
1615 in 1652 in
1616 case parse query e of 1653 case parse query e of
1617 NONE => default () 1654 SOME (Query1 r) =>
1618 | SOME r =>
1619 let 1655 let
1620 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => 1656 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1621 let 1657 let
1622 val (rvN, e) = rv rvN 1658 val (rvN, e) = rv rvN
1623 in 1659 in
1640 | SOME e => 1676 | SOME e =>
1641 case expIn (e, rvN) of 1677 case expIn (e, rvN) of
1642 (inr p', _) => And (p, p') 1678 (inr p', _) => And (p, p')
1643 | _ => p) 1679 | _ => p)
1644 end 1680 end
1681 | _ => default ()
1645 end 1682 end
1646 1683
1647 fun updateProp rvN rv e = 1684 fun updateProp rvN rv e =
1648 let 1685 let
1649 fun default () = (print ("Warning: Information flow checker can't parse SQL query at " 1686 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
1650 ^ ErrorMsg.spanToString (#2 e) ^ "\n"); 1687 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
1651 Unknown) 1688 Unknown)
1652 in 1689 in
1653 case parse query e of 1690 case parse query e of
1654 NONE => default () 1691 SOME (Query1 r) =>
1655 | SOME r =>
1656 let 1692 let
1657 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) => 1693 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
1658 let 1694 let
1659 val (rvN, e) = rv rvN 1695 val (rvN, e) = rv rvN
1660 in 1696 in
1685 | SOME e => 1721 | SOME e =>
1686 case expIn (e, rvN) of 1722 case expIn (e, rvN) of
1687 (inr p', _) => And (p, p') 1723 (inr p', _) => And (p, p')
1688 | _ => p) 1724 | _ => p)
1689 end 1725 end
1726 | _ => default ()
1690 end 1727 end
1691 1728
1692 fun evalPat env e (pt, _) = 1729 fun evalPat env e (pt, _) =
1693 case pt of 1730 case pt of
1694 PWild => (env, True) 1731 PWild => (env, True)
2065 val (st', r) = St.nextVar st 2102 val (st', r) = St.nextVar st
2066 val (st', acc) = St.nextVar st' 2103 val (st', acc) = St.nextVar st'
2067 2104
2068 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 2105 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
2069 2106
2070 val (st', qp, qwp, used, _) = 2107 val (st', qp, used, _) =
2071 queryProp env 2108 queryProp env
2072 st' (fn st' => 2109 st' (fn st' =>
2073 let 2110 let
2074 val (st', rv) = St.nextVar st' 2111 val (st', rv) = St.nextVar st'
2075 in 2112 in
2096 (St.setAmbient (st, p), Var out) 2133 (St.setAmbient (st, p), Var out)
2097 end 2134 end
2098 2135
2099 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st') 2136 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
2100 2137
2101 val p' = And (p', qwp) 2138 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
2102 val paths = map (fn e => ((loc, e, p'), Where)) used
2103 in 2139 in
2104 (res, St.addPaths (St.setSent (st, sent), paths)) 2140 (res, St.addPaths (St.setSent (st, sent), paths))
2105 end 2141 end
2106 | EDml e => 2142 | EDml e =>
2107 (case parse dml e of 2143 (case parse dml e of
2296 fun rv rvN = (rvN + 1, Lvar rvN) 2332 fun rv rvN = (rvN + 1, Lvar rvN)
2297 in 2333 in
2298 case pol of 2334 case pol of
2299 PolClient e => 2335 PolClient e =>
2300 let 2336 let
2301 val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e 2337 val (_, p, _, outs) = queryProp [] 0 rv SomeCol e
2302 in 2338 in
2303 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update) 2339 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
2304 end 2340 end
2305 | PolInsert e => 2341 | PolInsert e =>
2306 let 2342 let