diff options
| -rw-r--r-- | backend/CSE3.v | 7 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 24 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 4 |
3 files changed, 31 insertions, 4 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index e82b7cdb..d54b9ffa 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -67,14 +67,17 @@ End REWRITE. Definition transf_function (f: function) : res function := do tenv <- type_function f; - let (invariants, hints) := preanalysis tenv f in + let (invariants, hints) := preanalysis tenv f in let ctx := context_from_hints hints in + if check_inductiveness (ctx:=ctx) tenv invariants f + then OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); fn_code := PTree.map (transf_instr (ctx := ctx) invariants) f.(fn_code); - fn_entrypoint := f.(fn_entrypoint) |}. + fn_entrypoint := f.(fn_entrypoint) |} + else Error (msg "cse3: not inductive"). Definition transf_fundef (fd: fundef) : res fundef := AST.transf_partial_fundef transf_function fd. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 69c21113..43c44ccd 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -304,7 +304,7 @@ Section OPERATIONS. (rel : RELATION.t) : RELATION.t := store1 chunk addr (forward_move_l rel args) src ty rel. -Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := match instr with | Inop _ | Icond _ _ _ _ @@ -331,6 +331,28 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t Definition invariants := PMap.t RB.t. +Definition rel_le (x y : RELATION.t) : bool := (PSet.is_subset y x). + +Definition relb_le (x y : RB.t) : bool := + match x, y with + | None, _ => true + | (Some _), None => false + | (Some x), (Some y) => rel_le x y + end. + +Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.function) := + (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && + PTree_Properties.for_all (fn_code fn) + (fun pc instr => + match PMap.get pc inv with + | None => true + | Some rel => + let rel' := apply_instr pc tenv instr rel in + List.forallb + (fun pc' => relb_le rel' (PMap.get pc' inv)) + (RTL.successors_instr instr) + end). + Definition internal_analysis (tenv : typing_env) (f : RTL.function) : option invariants := DS.fixpoint diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 72b3e7e1..e277a3e1 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -76,7 +76,9 @@ Proof. destruct f; simpl; intros. - monadInv H. monadInv EQ. - destruct preanalysis. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. inv EQ1. reflexivity. - monadInv H. |