| Verification driver |
Require Import List TheoryList.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.AbsInt.Sal.
Require Import ProofOS.AbsInt.TypeSystem.
Require Import ProofOS.AbsInt.StackTypes.
Require Import ProofOS.AbsInt.SimpleTypes.
Set Implicit Arguments.
Module Type DRIVER_REGIONS.
Parameter minitMem : mem.
Parameter codeStart : int32.
Parameter codeLength : nat.
Axiom codeHigh : bvec_to_nat codeStart >= 4.
Axiom codeFits : bvec_to_nat codeStart + codeLength < pow2 32 - 3.
Axiom codeBigEnough : longestInstr + 1 <= codeLength.
Parameter stackStart : int32.
Parameter stackLength : nat.
Axiom stackHigh : bvec_to_nat stackStart >= 4.
Axiom stackBig : stackLength > 8.
Axiom stackFits : bvec_to_nat stackStart + stackLength < pow2 32 - 3.
Axiom stackCodeSeparate : disjointRegions codeStart codeLength stackStart stackLength.
Axiom stackLongEnough : stackLength >= 4.
End DRIVER_REGIONS.
Module Type DRIVER_PARAM.
Declare Module Regions : DRIVER_REGIONS.
Declare Module Sys : SIMPLE_TYPE_SYSTEM.
End DRIVER_PARAM.
Module Driver (Param : DRIVER_PARAM).
Import Param.
Import Regions.
Module StackParam <: M86_PARAM_FIXED_CODE_AND_STACK.
Definition minitState st := stPc st = codeStart /\ stMem st = minitMem.
Definition minitMem := minitMem.
Definition codeStart := codeStart.
Definition codeLength := codeLength.
Definition codeHigh := codeHigh.
Definition codeFits := codeFits.
Theorem pcInRange : forall st, minitState st
-> bvec_to_nat codeStart
<= bvec_to_nat (stPc st)
< bvec_to_nat codeStart + codeLength - longestInstr.
Theorem codeUniform : forall st, minitState st
-> agree_range (stMem st) minitMem codeStart codeLength.
Definition stackStart := stackStart.
Definition stackLength := stackLength.
Definition stackHigh := stackHigh.
Definition stackFits := stackFits.
Definition stackCodeSeparate := stackCodeSeparate.
End StackParam.
Module Simple := SimpleTypes.Make(StackParam).
Import Simple.
Import Stack.
Import TySys.
Import Fixed.
Import MySal.
Module MySys := Create(Sys).
Specify the root states for a verification |
Module Type ROOT_STATES.
Parameter roots : {rs : list (list (stateDescription (stackTy MySys.ty) (stackState MySys.ty unit))
* stateDescription (stackTy MySys.ty) (stackState MySys.ty unit))
| AllS (fun sd => match sdPc (snd sd) with
| ApcUnknown => False
| ApcConst pc => validPc pc
end) rs}.
Parameters functions : list (function_info (stackTy MySys.ty)).
End ROOT_STATES.
Module Make (Roots : ROOT_STATES).
Import Roots.
Module MyTypeSystemPlus <: TYPE_SYSTEM_WITH_FUNCTIONS.
Module Sys := MySys.
Definition functions := functions.
End MyTypeSystemPlus.
Module TypeSystem := Stack.AddStackTypes(MyTypeSystemPlus).
| Produce the first input to the chain of functors to come |
Module User <: USE_TYPE_SYSTEM.
Module Sys := TypeSystem.
Definition minit : {init : list (list (stateDescription Sys.ty Sys.mastate)
* stateDescription Sys.ty Sys.mastate)
| (AllS (fun sd => match sdPc (snd sd) with
| ApcUnknown => False
| ApcConst pc => validPc pc
end) init)
/\ forall st, M.minitState st -> exists ctx, exists sd,
In (nil, sd) init
/\ ApcConst (SstPc st) = sdPc sd
/\ (forall r, Sys.hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs sd)))
/\ Sys.mconc ctx st (sdCust sd)}.
End User.
Module Abs1 := Abstraction(User).
Module Abs2 := Fix(Abs1).
Module Ch := MySal.Checker(Abs2).
Module Mac := MC.
Definition verify := Ch.verify.
End Make.
Definition fold_right := fold_right.
End Driver.