Mercurial > urweb

comparison src/iflow.sml @ 1213:e791d93d4616

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
secret logon
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Apr 2010 16:14:19 -0400
parents fc33072c4d33
children 648e6b087dfb
comparison
equal deleted inserted replaced
1212:fc33072c4d33 1213:e791d93d4616
47 "attrifyString_w", 47 "attrifyString_w",
48 "attrifyChar_w", 48 "attrifyChar_w",
49 "urlifyInt_w", 49 "urlifyInt_w",
50 "urlifyFloat_w", 50 "urlifyFloat_w",
51 "urlifyString_w", 51 "urlifyString_w",
52 "urlifyBool_w"] 52 "urlifyBool_w",
53 "set_cookie"]
53 54
54 val writers = SS.addList (SS.empty, writers) 55 val writers = SS.addList (SS.empty, writers)
55 56
56 type lvar = int 57 type lvar = int
57 58
365 SOME e2 => eq' (e1, e2) 366 SOME e2 => eq' (e1, e2)
366 | NONE => 367 | NONE =>
367 if lvarIn n2 e1 then 368 if lvarIn n2 e1 then
368 false 369 false
369 else 370 else
370 (unif := IM.insert (!unif, n2, e1); 371 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
372 ("e1", p_exp e1)];*)
373 unif := IM.insert (!unif, n2, e1);
371 true)) 374 true))
372 375
373 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2) 376 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
374 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2) 377 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
375 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2 378 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
440 fun assert (t, e1, e2) = 443 fun assert (t, e1, e2) =
441 let 444 let
442 val r1 = lookup (t, e1) 445 val r1 = lookup (t, e1)
443 val r2 = lookup (t, e2) 446 val r2 = lookup (t, e2)
444 447
445 fun doUn (t', e1, e2) = 448 fun doUn k (t', e1, e2) =
446 case e2 of 449 case e2 of
447 Func (f, [e]) => 450 Func (f, [e]) =>
448 if String.isPrefix "un" f then 451 if String.isPrefix "un" f then
449 let 452 let
450 val f' = String.extract (f, 2, NONE) 453 val f' = String.extract (f, 2, NONE)
451 in 454 in
452 foldl (fn (e', t') => 455 foldl (fn (e', t') =>
453 case e' of 456 case e' of
454 Func (f'', [e'']) => 457 Func (f'', [e'']) =>
455 if f'' = f' then 458 if f'' = f' then
456 (lookup (t', e1), e'') :: t' 459 (lookup (t', e1), k e'') :: t'
457 else 460 else
458 t' 461 t'
459 | _ => t') t' (allPeers (t, e)) 462 | _ => t') t' (allPeers (t, e))
460 end 463 end
461 else 464 else
462 t' 465 t'
466 | Proj (e2, f) => doUn (fn e' => k (Proj (e', f))) (t', e1, e2)
463 | _ => t' 467 | _ => t'
464 in 468 in
465 if eq (r1, r2) then 469 if eq (r1, r2) then
466 t 470 t
467 else 471 else
468 doUn (doUn ((r1, r2) :: t, e1, e2), e2, e1) 472 doUn (fn x => x) (doUn (fn x => x) ((r1, r2) :: t, e1, e2), e2, e1)
469 end 473 end
470 474
471 open Print 475 open Print
472 476
473 fun query (t, e1, e2) = 477 fun query (t, e1, e2) =
556 (false, (Known, _)) => gls goals onFail 560 (false, (Known, _)) => gls goals onFail
557 | _ => 561 | _ =>
558 let 562 let
559 fun hps hyps = 563 fun hps hyps =
560 case hyps of 564 case hyps of
561 [] => onFail () 565 [] => ((*Print.preface ("Fail", p_prop (Reln g));*)
566 onFail ())
562 | ACond _ :: hyps => hps hyps 567 | ACond _ :: hyps => hps hyps
563 | AReln h :: hyps => 568 | AReln h :: hyps =>
564 let 569 let
565 val saved = save () 570 val saved = save ()
566 in 571 in
568 let 573 let
569 val changed = IM.numItems (!unif) 574 val changed = IM.numItems (!unif)
570 <> IM.numItems saved 575 <> IM.numItems saved
571 in 576 in
572 gls goals (fn () => (restore saved; 577 gls goals (fn () => (restore saved;
573 changed andalso hps hyps)) 578 changed (*andalso
579 (Print.preface ("Retry",
580 p_prop
581 (Reln g)
582 ); true)*)
583 andalso hps hyps))
574 end 584 end
575 else 585 else
576 hps hyps 586 hps hyps
577 end 587 end
578 in 588 in
1071 end 1081 end
1072 1082
1073 fun evalExp env (e as (_, loc), st as (nv, p, sent)) = 1083 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
1074 let 1084 let
1075 fun default () = 1085 fun default () =
1076 (Var nv, (nv+1, p, sent)) 1086 ((*Print.preface ("Default" ^ Int.toString nv,
1087 MonoPrint.p_exp MonoEnv.empty e);*)
1088 (Var nv, (nv+1, p, sent)))
1077 1089
1078 fun addSent (p, e, sent) = 1090 fun addSent (p, e, sent) =
1079 if isKnown e then 1091 if isKnown e then
1080 sent 1092 sent
1081 else 1093 else
1098 val (e, st) = evalExp env (e, st) 1110 val (e, st) = evalExp env (e, st)
1099 in 1111 in
1100 (Func ("Some", [e]), st) 1112 (Func ("Some", [e]), st)
1101 end 1113 end
1102 | EFfi _ => default () 1114 | EFfi _ => default ()
1115
1103 | EFfiApp (m, s, es) => 1116 | EFfiApp (m, s, es) =>
1104 if m = "Basis" andalso SS.member (writers, s) then 1117 if m = "Basis" andalso SS.member (writers, s) then
1105 let 1118 let
1106 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1119 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1107 in 1120 in
1113 let 1126 let
1114 val (es, st) = ListUtil.foldlMap (evalExp env) st es 1127 val (es, st) = ListUtil.foldlMap (evalExp env) st es
1115 in 1128 in
1116 (Func (m ^ "." ^ s, es), st) 1129 (Func (m ^ "." ^ s, es), st)
1117 end 1130 end
1118 | EApp _ => default () 1131
1132 | EApp (e1, e2) =>
1133 let
1134 val (e1, st) = evalExp env (e1, st)
1135 in
1136 case e1 of
1137 Finish => (Finish, st)
1138 | _ => default ()
1139 end
1140
1119 | EAbs _ => default () 1141 | EAbs _ => default ()
1120 | EUnop (s, e1) => 1142 | EUnop (s, e1) =>
1121 let 1143 let
1122 val (e1, st) = evalExp env (e1, st) 1144 val (e1, st) = evalExp env (e1, st)
1123 in 1145 in
1249 (res, (nvs, p, sent)) 1271 (res, (nvs, p, sent))
1250 end 1272 end
1251 | EDml _ => default () 1273 | EDml _ => default ()
1252 | ENextval _ => default () 1274 | ENextval _ => default ()
1253 | ESetval _ => default () 1275 | ESetval _ => default ()
1276
1277 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
1278 (Var nv, (nv + 1, And (p, Reln (Known, [Var nv])), sent))
1254 1279
1255 | EUnurlify _ => default () 1280 | EUnurlify _ => default ()
1256 | EJavaScript _ => default () 1281 | EJavaScript _ => default ()
1257 | ESignalReturn _ => default () 1282 | ESignalReturn _ => default ()
1258 | ESignalBind _ => default () 1283 | ESignalBind _ => default ()
1263 | ESpawn _ => default () 1288 | ESpawn _ => default ()
1264 end 1289 end
1265 1290
1266 fun check file = 1291 fun check file =
1267 let 1292 let
1293 val file = MonoReduce.reduce file
1294 val file = MonoOpt.optimize file
1295 val file = Fuse.fuse file
1296 val file = MonoOpt.optimize file
1297 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
1298
1268 val exptd = foldl (fn ((d, _), exptd) => 1299 val exptd = foldl (fn ((d, _), exptd) =>
1269 case d of 1300 case d of
1270 DExport (_, _, n, _, _, _) => IS.add (exptd, n) 1301 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
1271 | _ => exptd) IS.empty file 1302 | _ => exptd) IS.empty file
1272 1303
1300 1331
1301 val (vals, pols) = foldl decl ([], []) file 1332 val (vals, pols) = foldl decl ([], []) file
1302 in 1333 in
1303 app (fn (loc, e, p) => 1334 app (fn (loc, e, p) =>
1304 let 1335 let
1305 val p = And (p, Reln (Eq, [Var 0, e])) 1336 fun doOne e =
1337 let
1338 val p = And (p, Reln (Eq, [Var 0, e]))
1339 in
1340 if List.exists (fn pol => if imply (p, pol) then
1341 (if !debug then
1342 Print.prefaces "Match"
1343 [("Hyp", p_prop p),
1344 ("Goal", p_prop pol)]
1345 else
1346 ();
1347 true)
1348 else
1349 false) pols then
1350 ()
1351 else
1352 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1353 Print.preface ("The state satisifes this predicate:", p_prop p))
1354 end
1355
1356 fun doAll e =
1357 case e of
1358 Const _ => ()
1359 | Var _ => doOne e
1360 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
1361 | Func (f, es) => if String.isPrefix "un" f then
1362 doOne e
1363 else
1364 app doAll es
1365 | Recd xes => app (doAll o #2) xes
1366 | Proj _ => doOne e
1367 | Finish => ()
1306 in 1368 in
1307 if List.exists (fn pol => if imply (p, pol) then 1369 doAll e
1308 (if !debug then
1309 Print.prefaces "Match"
1310 [("Hyp", p_prop p),
1311 ("Goal", p_prop pol)]
1312 else
1313 ();
1314 true)
1315 else
1316 false) pols then
1317 ()
1318 else
1319 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1320 Print.preface ("The state satisifes this predicate:", p_prop p))
1321 end) vals 1370 end) vals
1322 end 1371 end
1323 1372
1373 val check = fn file =>
1374 let
1375 val oldInline = Settings.getMonoInline ()
1376 in
1377 (Settings.setMonoInline (case Int.maxInt of
1378 NONE => 1000000
1379 | SOME n => n);
1380 check file;
1381 Settings.setMonoInline oldInline)
1382 handle ex => (Settings.setMonoInline oldInline;
1383 raise ex)
1384 end
1385
1324 end 1386 end
1387