Mercurial > urweb

comparison src/iflow.sml @ 1233:8d1d2f7163c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix problem with overly weak ambients for queries; fix known-related bug in assert for Dt1
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 10:40:55 -0400
parents efbefd6e3f6c
children e799c8df3146
comparison
equal deleted inserted replaced
1232:efbefd6e3f6c 1233:8d1d2f7163c2
785 | Nothing => 785 | Nothing =>
786 let 786 let
787 val r'' = ref (Node {Rep = ref NONE, 787 val r'' = ref (Node {Rep = ref NONE,
788 Cons = ref SM.empty, 788 Cons = ref SM.empty,
789 Variety = Nothing, 789 Variety = Nothing,
790 Known = ref false}) 790 Known = ref (!(#Known (unNode r)))})
791 791
792 val r' = ref (Node {Rep = ref NONE, 792 val r' = ref (Node {Rep = ref NONE,
793 Cons = ref SM.empty, 793 Cons = ref SM.empty,
794 Variety = Dt1 (f, r''), 794 Variety = Dt1 (f, r''),
795 Known = ref false}) 795 Known = #Known (unNode r)})
796 in 796 in
797 #Rep (unNode r) := SOME r' 797 #Rep (unNode r) := SOME r'
798 end 798 end
799 | _ => raise Contradiction 799 | _ => raise Contradiction
800 end 800 end
2107 val orig = St.ambient st 2107 val orig = St.ambient st
2108 val origPaths = St.paths st 2108 val origPaths = St.paths st
2109 2109
2110 val st = St.addPath (st, ((loc, e, orig), Case)) 2110 val st = St.addPath (st, ((loc, e, orig), Case))
2111 2111
2112 val (st, paths) = 2112 (*val () = Print.prefaces "Case" [("loc", Print.PD.string (ErrorMsg.spanToString loc)),
2113 foldl (fn ((pt, pe), (st, paths)) => 2113 ("e", Print.p_list (MonoPrint.p_exp MonoEnv.empty o #2) pes),
2114 ("orig", p_prop orig)]*)
2115
2116 val (st, ambients, paths) =
2117 foldl (fn ((pt, pe), (st, ambients, paths)) =>
2114 let 2118 let
2115 val (env, pp) = evalPat env e pt 2119 val (env, pp) = evalPat env e pt
2116 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp))) 2120 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
2117 2121
2118 val this = And (removeRedundant orig (St.ambient st'), 2122 val this = And (removeRedundant orig (St.ambient st'),
2119 Reln (Eq, [Var r, pe])) 2123 Reln (Eq, [Var r, pe]))
2120 in 2124 in
2121 (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths), 2125 (St.setPaths (st', origPaths),
2126 Or (ambients, this),
2122 St.paths st' @ paths) 2127 St.paths st' @ paths)
2123 end) (St.setAmbient (st, False), []) pes 2128 end) (st, False, []) pes
2124 2129
2125 val st = case #1 res of 2130 val st = case #1 res of
2126 TRecord [] => St.setPaths (st, origPaths) 2131 TRecord [] => St.setPaths (st, origPaths)
2127 | _ => St.setPaths (st, paths) 2132 | _ => St.setPaths (st, paths)
2128 in 2133 in
2129 (Var r, St.setAmbient (st, And (orig, St.ambient st))) 2134 (Var r, St.setAmbient (st, And (orig, ambients)))
2130 end 2135 end
2131 | EStrcat (e1, e2) => 2136 | EStrcat (e1, e2) =>
2132 let 2137 let
2133 val (e1, st) = evalExp env (e1, st) 2138 val (e1, st) = evalExp env (e1, st)
2134 val (e2, st) = evalExp env (e2, st) 2139 val (e2, st) = evalExp env (e2, st)
2181 2186
2182 val (st', r) = St.nextVar st 2187 val (st', r) = St.nextVar st
2183 val (st', acc) = St.nextVar st' 2188 val (st', acc) = St.nextVar st'
2184 2189
2185 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st') 2190 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
2191 val amb = removeRedundant (St.ambient st) (St.ambient st')
2186 2192
2187 val (st', qp, used, _) = 2193 val (st', qp, used, _) =
2188 queryProp env 2194 queryProp env
2189 st' (fn st' => 2195 st' (fn st' =>
2190 let 2196 let
2192 in 2198 in
2193 (st', Var rv) 2199 (st', Var rv)
2194 end) 2200 end)
2195 (AllCols (Var r)) q 2201 (AllCols (Var r)) q
2196 2202
2197 val p' = And (qp, St.ambient st')
2198
2199 val (st, res) = if varInP acc (St.ambient st') then 2203 val (st, res) = if varInP acc (St.ambient st') then
2200 let 2204 let
2201 val (st, r) = St.nextVar st 2205 val (st, r) = St.nextVar st
2202 in 2206 in
2203 (st, Var r) 2207 (st, Var r)
2204 end 2208 end
2205 else 2209 else
2206 let 2210 let
2207 val (st, out) = St.nextVar st' 2211 val (st', out) = St.nextVar st'
2208 2212
2209 val p = Or (Reln (Eq, [Var out, i]), 2213 val p = And (St.ambient st,
2210 And (Reln (Eq, [Var out, b]), 2214 Or (Reln (Eq, [Var out, i]),
2211 p')) 2215 And (Reln (Eq, [Var out, b]),
2216 And (qp, amb))))
2212 in 2217 in
2213 (St.setAmbient (st, p), Var out) 2218 (St.setAmbient (st', p), Var out)
2214 end 2219 end
2215 2220
2216 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st') 2221 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
2217 2222
2223 val p' = And (qp, St.ambient st')
2218 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used 2224 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
2219 in 2225 in
2220 (res, St.addPaths (St.setSent (st, sent), paths)) 2226 (res, St.addPaths (St.setSent (st, sent), paths))
2221 end 2227 end
2222 | EDml e => 2228 | EDml e =>
2506 fun relevant () = 2512 fun relevant () =
2507 let 2513 let
2508 val avail = foldl (fn (AReln (Sql tab, _), avail) => 2514 val avail = foldl (fn (AReln (Sql tab, _), avail) =>
2509 SS.add (avail, tab) 2515 SS.add (avail, tab)
2510 | (_, avail) => avail) SS.empty hyps 2516 | (_, avail) => avail) SS.empty hyps
2517
2518 val ls = List.filter
2519 (fn (g1, _) =>
2520 decompG g1
2521 (List.all (fn AReln (Sql tab, _) =>
2522 SS.member (avail, tab)
2523 | _ => true))) client
2511 in 2524 in
2512 List.filter 2525 (*print ("Max: " ^ Int.toString (length ls) ^ "\n");*)
2513 (fn (g1, _) => 2526 ls
2514 decompG g1
2515 (List.all (fn AReln (Sql tab, _) =>
2516 SS.member (avail, tab)
2517 | _ => true))) client
2518 end 2527 end
2519 2528
2520 fun tryCombos (maxLv, pols, g, outs) = 2529 fun tryCombos (maxLv, pols, g, outs) =
2521 case pols of 2530 case pols of
2522 [] => 2531 [] =>
2549 ^ (case fl of 2558 ^ (case fl of
2550 Control Where => " (WHERE clause)" 2559 Control Where => " (WHERE clause)"
2551 | Control Case => " (case discriminee)" 2560 | Control Case => " (case discriminee)"
2552 | Data => " (returned data value)"), 2561 | Data => " (returned data value)"),
2553 Print.p_list p_atom hyps); 2562 Print.p_list p_atom hyps);
2563 Print.preface ("DB", Cc.p_database cc);
2554 false) 2564 false)
2555 end handle Cc.Contradiction => true) then 2565 end handle Cc.Contradiction => true) then
2556 () 2566 ()
2557 else 2567 else
2558 ErrorMsg.errorAt loc "The information flow policy may be violated here." 2568 ErrorMsg.errorAt loc "The information flow policy may be violated here."