(* * 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) *) Set Implicit Arguments. Require Import hpattern vgtac. Require Import Global UserProofType DStr Syn. Require DomCon SemCon DomSen. Require Import SemCommon. Module Make (Import PInput : PINPUT). Local Open Scope type. Module Dom := DomSen.Make PInput. Include Dom. Section Sem. Variable g : G.t. Let pgm : InterCfg.t := G.icfg g. Let mode : UserInputType.update_mode := UserInputType.Strong. Definition postfix_cmd (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := forall cmd (Hcmd : Some cmd = InterCfg.get_cmd pgm cn), let m := s (cn, Inputof, calls) in let m' := run_only mode g cn cmd m in Mem.le m' (s (cn, Outputof, calls)). Definition postfix_intra_edge (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := let p := InterNode.get_pid cn in let n := InterNode.get_node cn in forall n' cfg (Hcfg : InterCfg.PidMap.MapsTo p cfg (InterCfg.cfgs pgm)) (Hedge : IntraCfg.is_succ cfg n n') (Hcn_cond: not (InterCfg.is_call_node pgm cn)), Mem.le (s (cn, Outputof, calls)) (s ((p, n'), 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)), Mem.le (s (cn, Outputof, calls)) (s ((callee, IntraNode.Entry), Inputof, cn :: calls)). Definition postfix_inter_ret (cn : InterNode.t) (calls : list InterNode.t) (s : state_t) : Prop := forall p (Hp : cn = (p, IntraNode.Exit)) cn' (Hedge : InterCfg.is_succ pgm cn cn') calln (Hret: Some cn' = InterCfg.returnof pgm calln), Mem.le (s (cn, Outputof, calln :: calls)) (s (cn', Inputof, calls)). Definition postfix (s : state_t) : Prop := forall (cn : InterNode.t) (calls : list InterNode.t) (Hreach : InterCfg.reachables pgm calls (InterNode.get_pid cn)), postfix_cmd cn calls s /\ postfix_intra_edge cn calls s /\ postfix_inter_call cn calls s /\ postfix_inter_ret cn calls s. End Sem. Local Close Scope type. End Make.