Mercurial > urweb

comparison src/iflow.sml @ 1228:7dfa67560916

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Using multiple policies to check a written value
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 16:46:38 -0400
parents 1d8fba74e7f5
children a2cd6664f57f
comparison
equal deleted inserted replaced
1227:1d8fba74e7f5 1228:7dfa67560916
306 | Or (p1, p2) => lvi p1 orelse lvi p2 306 | Or (p1, p2) => lvi p1 orelse lvi p2
307 | Reln (_, es) => List.exists (varIn lv) es 307 | Reln (_, es) => List.exists (varIn lv) es
308 | Cond (e, p) => varIn lv e orelse lvi p 308 | Cond (e, p) => varIn lv e orelse lvi p
309 in 309 in
310 lvi 310 lvi
311 end
312
313 fun bumpLvars by =
314 let
315 fun lvi e =
316 case e of
317 Const _ => e
318 | Var _ => e
319 | Lvar lv => Lvar (lv + by)
320 | Func (f, es) => Func (f, map lvi es)
321 | Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes)
322 | Proj (e, f) => Proj (lvi e, f)
323 | Finish => e
324 in
325 lvi
326 end
327
328 fun bumpLvarsP by =
329 let
330 fun lvi p =
331 case p of
332 True => p
333 | False => p
334 | Unknown => p
335 | And (p1, p2) => And (lvi p1, lvi p2)
336 | Or (p1, p2) => And (lvi p1, lvi p2)
337 | Reln (r, es) => Reln (r, map (bumpLvars by) es)
338 | Cond (e, p) => Cond (bumpLvars by e, lvi p)
339 in
340 lvi
341 end
342
343 fun maxLvar e =
344 let
345 fun lvi e =
346 case e of
347 Const _ => 0
348 | Var _ => 0
349 | Lvar lv => lv
350 | Func (f, es) => foldl Int.max 0 (map lvi es)
351 | Recd xes => foldl Int.max 0 (map (lvi o #2) xes)
352 | Proj (e, f) => lvi e
353 | Finish => 0
354 in
355 lvi e
356 end
357
358 fun maxLvarP p =
359 let
360 fun lvi p =
361 case p of
362 True => 0
363 | False => 0
364 | Unknown => 0
365 | And (p1, p2) => Int.max (lvi p1, lvi p2)
366 | Or (p1, p2) => Int.max (lvi p1, lvi p2)
367 | Reln (r, es) => foldl Int.max 0 (map maxLvar es)
368 | Cond (e, p) => Int.max (maxLvar e, lvi p)
369 in
370 lvi p
311 end 371 end
312 372
313 fun eq' (e1, e2) = 373 fun eq' (e1, e2) =
314 case (e1, e2) of 374 case (e1, e2) of
315 (Const p1, Const p2) => Prim.equal (p1, p2) 375 (Const p1, Const p2) => Prim.equal (p1, p2)
2388 let 2448 let
2389 val p = And (p, Reln (Eq, [Var 0, e])) 2449 val p = And (p, Reln (Eq, [Var 0, e]))
2390 in 2450 in
2391 if decompH p 2451 if decompH p
2392 (fn hyps => 2452 (fn hyps =>
2393 (fl <> Control Where 2453 let
2394 andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) 2454 val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab)
2395 orelse List.exists (fn (p', outs) => 2455 | (_, avail) => avail) SS.empty hyps
2396 decompG p' 2456
2397 (fn goals => imply (hyps, goals, SOME outs))) 2457 fun tryCombos (maxLv, pols, g, outs) =
2398 client) then 2458 case pols of
2459 [] =>
2460 decompG g
2461 (fn goals => imply (hyps, goals, SOME outs))
2462 | (g1, outs1) :: pols =>
2463 let
2464 val g1 = bumpLvarsP (maxLv + 1) g1
2465 val outs1 = map (bumpLvars (maxLv + 1)) outs1
2466 fun skip () = tryCombos (maxLv, pols, g, outs)
2467 in
2468 if decompG g1
2469 (List.all (fn AReln (Sql tab, _) =>
2470 SS.member (avail, tab)
2471 | _ => true)) then
2472 skip ()
2473 orelse tryCombos (Int.max (maxLv,
2474 maxLvarP g1),
2475 pols,
2476 And (g1, g),
2477 outs1 @ outs)
2478 else
2479 skip ()
2480 end
2481 in
2482 (fl <> Control Where
2483 andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
2484 orelse List.exists (fn (p', outs) =>
2485 decompG p'
2486 (fn goals => imply (hyps, goals, SOME outs)))
2487 client
2488 orelse tryCombos (0, client, True, [])
2489 orelse (reset ();
2490 Print.preface ("Untenable hypotheses",
2491 Print.p_list p_atom hyps);
2492 false)
2493 end) then
2399 () 2494 ()
2400 else 2495 else
2401 (ErrorMsg.errorAt loc "The information flow policy may be violated here."; 2496 ErrorMsg.errorAt loc "The information flow policy may be violated here."
2402 Print.preface ("The state satisifies this predicate:", p_prop p))
2403 end 2497 end
2404 2498
2405 fun doAll e = 2499 fun doAll e =
2406 case e of 2500 case e of
2407 Const _ => () 2501 Const _ => ()