(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) (** * Abstract semantics (context-sen + localized) *) Set Implicit Arguments. Require Import hpattern vgtac. Require Import Global UserProofType DStr Syn. Require DomCon SemCon DomSen SemSen. Require Import SemCommon. Module Make (Import PInput : PINPUT). Local Open Scope type. Module Sen := SemSen.Make PInput. Include Sen.Dom. Section Sem. Variable g : G.t. Let pgm : InterCfg.t := G.icfg g. Let mode : UserInputType.update_mode := UserInputType.Strong. Variable amap : access_map. Definition postfix_cmd (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := Sen.postfix_cmd g cn calls s. Definition postfix_intra_edge (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := Sen.postfix_intra_edge g cn calls s. Definition postfix_intra_call (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := forall callee (Hedge : InterCfg.is_succ pgm cn (callee, IntraNode.Entry)) retn (Hretn : Some retn = InterCfg.returnof pgm cn), let access := get_all_access callee amap in let m := (s (cn, Outputof, calls)) in let m' := Mem.subtract access m in Mem.le m' (s (retn, Inputof, calls)). Definition postfix_inter_call (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := forall callee (Hedge : InterCfg.is_succ pgm cn (callee, IntraNode.Entry)), let access := get_all_access callee amap in let m := (s (cn, Outputof, calls)) in let m' := Mem.restrict access m in Mem.le m' (s ((callee, IntraNode.Entry), Inputof, cn :: calls)). Definition postfix_inter_ret (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := Sen.postfix_inter_ret g cn calls s. Definition postfix (s : state_t) : Prop := forall (cn : InterNode.t) (calls : list InterNode.t), postfix_cmd cn calls s /\ postfix_intra_edge cn calls s /\ postfix_intra_call cn calls s /\ postfix_inter_call cn calls s /\ postfix_inter_ret cn calls s. Definition sound_amap_run (s : state_t) := forall cn calls cmd (Hcmd : Some cmd = InterCfg.get_cmd pgm cn), Acc.le (Acc.get_acc (run_access mode g cn cmd (s (cn, SemCommon.Inputof, calls)))) (get_access (InterNode.get_pid cn) amap). Definition sound_amap_reachable := forall f1 f2 (Hr : InterCfg.reachable pgm f1 f2), Acc.le (get_access f2 amap) (get_access f1 amap). Definition sound_amap (s : state_t) := sound_amap_run s /\ sound_amap_reachable. End Sem. Local Close Scope type. End Make.