-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- File: tscheck.d
-- Author: Rob Strom
-- SCCS Info: @(#)tscheck.d	1.1 7/27/89

tscheck: USING(Positions, Coercions, Errors, InferredType, Typestate_Inference, Checking_Table, AbsFormat, Stdenv) 
definitions

-- CheckClause
-- This procedure scans a clause and does all these things:
-- 1. It adds coercions before any statement which needs them.
-- 2. It checks each statement for typestate correctness.
-- 3. It records each exception branch.
-- 4. It updates the typestate on each exception branch destination.
CheckClauseCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Clause: ClauseId, -- identifies clause being checked
  EntryTS: Typestate, -- typestate on entry to the clause
  ExitTS: Typestate, -- typestate on normal exit, if there is one
  Context: TypestateCheckingEnvironment -- local state
)
CONSTANT(Services, Code, Definitions, Clause, EntryTS)
EXIT  {Full}
MINIMUM {Full(Services), Full(Code), Full(Definitions), Full(Clause), Full(EntryTS), Full(Context)}
EXCEPTION NoNormalExit -- raised if clause ends with an exit statement or with a block with no normal exit
  {Full(Services), Full(Code), Full(Definitions), Full(Clause), Full(EntryTS), Full(Context)}
;
CheckClauseInport: INPORT OF CheckClauseCall
{Full(Services), Full(Code),  Full(Definitions), Full(Clause), Full(EntryTS), Full(Context)};
CheckClauseOutport: OUTPORT OF CheckClauseInport;
 
-- CheckGuardClause
-- This procedure checks WHERE, WHILE, IF clauses.
-- It verifies that (a) the clause has a normal exit,
--  and (b) that the result object is INIT
-- Can generate DeadCode and NotAsserted errors
CheckGuardClauseCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Clause: ClauseId, -- identifies clause being checked
  Position: Aposition, -- position of statement containing clause
  Result: ObjectName, -- object expected to be INIT
  EntryTS: Typestate, -- typestate on entry to the clause
  ExitTS: Typestate, -- typestate on normal exit, if there is one
  Context: TypestateCheckingEnvironment -- local state
)
CONSTANT(Services, Code, Definitions, Clause, Position, Result, EntryTS)
EXIT  {Full}
MINIMUM {Full(Services), Full(Code), Full(Definitions), Full(Clause), Full(Position), Full(Result), Full(EntryTS), Full(Context)}
EXCEPTION NoNormalExit -- raised if clause ends with an exit statement or with a block with no normal exit
  {Full(Services), Full(Code), Full(Definitions), Full(Clause), Full(Position), Full(Result), Full(EntryTS), Full(Context)}
;
CheckGuardClauseInport: INPORT OF CheckGuardClauseCall
{Full(Services), Full(Code),  Full(Definitions), Full(Clause), Full(Position), Full(Result), Full(EntryTS), Full(Context)};
CheckGuardClauseOutport: OUTPORT OF CheckGuardClauseInport;
 
-- Determine Precondition
-- This is a class of functions
-- The actual functions called are determined by table lookup
-- The typestate precondition includes 
-- required attributes, and forbidden attributes.
-- The precondition may depend upon the current typestate.
-- For example, if an object must be without constraints, it is necessary
-- to know what constraints it has now in order to know what constraints
-- must be dropped.
-- These functions also check VAR and POS context-dependent requirements,
-- and will report errors if these requirements are violated.
DeterminePreconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Definitions: Definitions_Modules, -- definitions used by program
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- local state
  Statement: Statement, -- Statement whose precondition is required
  Position: Aposition, -- location of statement (in case error msg is generated)
  CurrentTS: Typestate, -- typestate at point where statement is executed
  Affected_Operands: Operand_Offsets, -- information from table specifying which operands to examine
  Required: Typestate, -- attributes which must be in TS
  Forbidden: Typestate -- attributes which must not be in TS
)
CONSTANT(Services, Definitions, Declarations, Statement, Position, CurrentTS, Affected_Operands)
EXIT{full}
MINIMUM{full}
;
DeterminePreconditionInport: INPORT OF DeterminePreconditionCall {full};
DeterminePreconditionOutport: OUTPORT OF DeterminePreconditionInport;
 
-- ApplyPrecondition
-- This procedure coerces the typestate down to meet the precondition.
-- This procedure checks for NotAsserted and NotLowerable.
-- If one of these errors is detected, the procedure "guesses" an appropriate
-- typestate.  Checking will continue, but the usefulness of future
-- messages will depend upon the guess.
ApplyPreconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Position: Aposition, -- location of statement (in case error msg is generated)
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Required: Typestate, -- attributes which must be in TS
  Forbidden: Typestate, -- attributes which must not be in TS
  CurrentTS: Typestate -- updated typestate
)
CONSTANT(Services, Declarations, Definitions, Position)
EXIT{full}
MINIMUM{full}
;
ApplyPreconditionInport: INPORT OF ApplyPreconditionCall {full};
ApplyPreconditionOutport: OUTPORT OF ApplyPreconditionInport;
 
-- Determine CALL Postcondition
-- This procedure computes the changes to the postcondition
-- resulting from the call statement
DetermineCallPostconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate checking environment
  Definitions: Definitions_Modules, -- definitions used by program
  Statement: Statement, -- Statement whose precondition is required
  CurrentTS: Typestate, -- typestate at point where statement is executed
  NormalPostcondition: AddDropSet, -- changes to TS for normal outcome
  ExceptionPostconditions: AddDropSets -- changes to TS for exception outcome
)
CONSTANT(Services, Declarations, Context, Definitions, Statement, CurrentTS)
EXIT{full}
MINIMUM {full(Services), Full(Declarations), Full(Context), Full(Definitions), Full(Statement), Full(CurrentTS)}
EXCEPTION NoPostcondition
  {full(Services), Full(Declarations), Full(Context), Full(Definitions), Full(Statement), Full(CurrentTS)}
;
DetermineCallPostconditionInport: INPORT OF DetermineCallPostconditionCall {Full(Services), Full(Declarations), Full(Context), Full(Definitions), Full(Statement), Full(CurrentTS)};
DetermineCallPostconditionOutport: OUTPORT OF DetermineCallPostconditionInport;
 
-- This procedure computes the typestate changes
-- resulting from executing this statement.
-- As with the precondition, the postcondition may depend on the
-- current typestate.
-- Each rule inserts attributes into the adds or drops sets
DeterminePostconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate checking environment
  Definitions: Definitions_Modules, -- definitions used by program
  Statement: Statement, -- Statement whose precondition is required
  CurrentTS: Typestate, -- typestate at point where statement is executed
  Affected_Operands: Operand_Offsets, -- information from table specifying which operands to examine
  NormalPostcondition: AddDropSet -- changes to TS for normal outcome
)
CONSTANT(Services, Declarations, Context, Definitions, Statement, CurrentTS, Affected_Operands)
EXIT{full} MINIMUM{full}
;
DeterminePostconditionInport: INPORT OF DeterminePostconditionCall {Full};
DeterminePostconditionOutport: OUTPORT OF DeterminePostconditionInport;
 
-- Apply Postcondition
-- This procedure takes a typestate and a postcondition's typestate
-- changes, and produces the changed typestate.
-- This procedure may raise the error 'CannotAdd' or 'CannotDrop'.
-- If this happens, some "guessed" typestate is produced and checking continues.
ApplyPostconditionCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Position: Aposition, -- location of statement (in case error msg is generated)
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  PostCondition: AddDropSet, -- changes to TS
  CurrentTS: Typestate -- typestate before and after operation
)
CONSTANT(Services, Declarations, Definitions, Position)
EXIT{full}
MINIMUM{full};
ApplyPostconditionInport: INPORT OF ApplyPostconditionCall {full};
ApplyPostconditionOutport: OUTPORT OF ApplyPostconditionInport;

-- Add or Drop Attribute
-- This procedure adds or drops a single attribute from current TS and checks
-- whether this results in an impossible typestate
AddDropCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Position: Aposition, -- location of statement (in case error msg is generated)
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  PostCondition: AddDropSet, -- changes to TS
  CurrentTS: Typestate, -- typestate before and after operation
  Attribute: Attribute -- attribute being added or dropped
)
CONSTANT(Services, Declarations, Definitions, Position, Attribute)
EXIT{full}
MINIMUM {full}
EXCEPTION Illegal -- raised if impossible typestate would result
{full}
;
AddDropInport: INPORT OF AddDropCall {full};
AddDropOutport: OUTPORT OF AddDropInport;


-- Attempt to Coerce
-- This procedure takes a current typestate and an attribute to be dropped
-- and determines:
-- 1. the coercion operator and operand for the coercion to drop the attribute
-- 2. the set of attributes which must be dropped before the coercion can be applied (the Prerequisites)
-- 3. the set of attributes which will be dropped together by applying the coercion (the Corequisites, including the requested attribute)
-- NB: Transitive prerequisites (prerequisites of prerequisites) are not
-- returned.  To get them, it is necessary to re-invoke this procedure.
AttemptToCoerceCall:  CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Definitions: Definitions_Modules, -- definitions used by program
  DroppedAttribute: Attribute, -- attribute being dropped
  CurrentTS: Typestate, -- typestate before coercion
  Coercion: Statement, -- the statement which drops the attribute
  Prerequisites: Typestate, -- the set of attributes which must be dropped before coercion can be applied
  Corequisites: Typestate -- the set of attributes dropped by coercion
)
CONSTANT(Services, Declarations, Definitions, DroppedAttribute, CurrentTS)
EXIT{full}
MINIMUM{full(Services), full(Declarations),  full(Context), full(Definitions), full(DroppedAttribute), full(CurrentTS)};
AttemptToCoerceInport: INPORT OF AttemptToCoerceCall {full(Services), full(Declarations),  full(Context), full(Definitions), full(DroppedAttribute), full(CurrentTS)};
AttemptToCoerceOutport:  OUTPORT OF AttemptToCoerceInport;

-- Involving
-- This procedure determines
-- the attributes which must be dropped from CurrentTS 
-- in order that a given Object has precisely the set of attributes in AttributeList and no others
InvolvingCall: CALLMESSAGE(
  CurrentTS: Typestate, -- typestate 
  Object: Objectname, -- object required to have AttributeList
  AttributeList: Typestate, -- the set of attributes needed to perform some operation
  Prerequisites: Typestate -- the set of attributes which must be dropped before operation can be applied
)
CONSTANT(CurrentTS, Object, AttributeList)
EXIT{full};
InvolvingInport: INPORT OF InvolvingCall {full(CurrentTS), full(Object), full(AttributeList)};
InvolvingOutport: OUTPORT OF InvolvingInport; 
  
 
-- Exception Branch
-- This procedure records a branch from a statement to a handler.
-- It determines where the handler is by searching back through the path.
-- It computes the soft coercions needed at the branch target.
ExceptionBranchCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Exception: Handlername, -- the exception which is raised
  CurrentTS: Typestate -- typestate where exception was raised
)
CONSTANT(Services, Declarations, Definitions, Exception, CurrentTS)
EXIT{full}
MINIMUM{full};
ExceptionBranchInport: INPORT OF ExceptionBranchCall {full};
ExceptionBranchOutport: OUTPORT OF ExceptionBranchInport;

BeginAlternativesCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  NextAlternative: NextAlternativeOutport, --  function to accumulate knowledge about each clause
  EndAlternatives: EndAlternativesOutport, -- common function to execute when all alternatives complete
  NullAlternative: NullAlternativeOutport -- variant of NextAlternative for Empty Clause (artifact of IF not always having an ELSE clause)
  )
CONSTANT(Services)
EXIT{full};
BeginAlternativesInport: INPORT OF BeginAlternativesCall {full(Services)};
BeginAlternativesOutport: OUTPORT OF BeginAlternativesInport;

NullAlternativeCall: CALLMESSAGE(
  Services: TypestateCheckingServices, 
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  EntryTS: Typestate, -- typestate on entry to the clause
  Context: TypestateCheckingEnvironment -- knowledge needed to check clause
         -- and knowledge needed as input to translation phase
)
CONSTANT(Services, Code, Definitions, EntryTS)
EXIT {full}
MINIMUM{full};
NullAlternativeInport:  INPORT OF NullAlternativeCall {full};
NullAlternativeOutport: OUTPORT OF NullAlternativeInport;

NextAlternativeCall: CALLMESSAGE(
  Services: TypestateCheckingServices, 
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Clause: ClauseId, -- clause containing alternative
  EntryTS: Typestate, -- typestate on entry to the clause
  Context: TypestateCheckingEnvironment -- knowledge needed to check clause
         -- and knowledge needed as input to translation phase
)
CONSTANT(Services, Code, Definitions, Clause, EntryTS)
EXIT {full}
MINIMUM {full};
NextAlternativeInport:  INPORT OF NextAlternativeCall {full};
NextAlternativeOutport: OUTPORT OF NextAlternativeInport;

EndAlternativesCall: CALLMESSAGE(
  Services: TypestateCheckingServices, 
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Context: TypestateCheckingEnvironment, -- knowledge needed to check clause
         -- and knowledge needed as input to translation phase
  Position: Aposition, -- location of statement after which coercions are to be inserted
  ExitTS: Typestate -- typestate on normal exit, if there is one
)
CONSTANT(Services, Code, Definitions, Position)
EXIT
  {Full}
MINIMUM {Full(Services), Full(Code), Full(Definitions), Full(Context), Full(Position)}
EXCEPTION NoNormalExit -- raised if clause ends with an exit statement or with a block with no normal exit
  {Full(Services), Full(Code), Full(Definitions), Full(Context), Full(Position)};
EndAlternativesInport: INPORT OF EndAlternativesCall {Full(Services), Full(Code), Full(Definitions), Full(Context), Full(Position)};
EndAlternativesOutport: OUTPORT OF EndAlternativesInport;

-- procedure to determine if a missing attribute is implied by INIT(CM)
ImpliedAttributeCall: CALLMESSAGE (
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Attribute: Attribute, -- attribute being checked
  CurrentTS: Typestate, -- current typestate
  Implied: Boolean  -- the attribute is implied
  )
CONSTANT(Services, Declarations, Definitions, Context, Attribute, CurrentTS)
EXIT{full};
ImpliedAttributeInport: INPORT OF ImpliedAttributeCall {Full(Services), full(Declarations), full(Definitions), full(Context), full(Attribute), full(CurrentTS)};
ImpliedAttributeOutport: OUTPORT OF ImpliedAttributeInport;

-- CheckVar
-- procedure to check that an object is VAR
CheckVarCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Definitions: Definitions_Modules, -- definitions used by program
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- local state
  Object: Objectname, -- Object being checked for VAR
  Position: Aposition -- location of statement (in case error msg is generated)
)
CONSTANT(Services, Definitions, Declarations, Object, Position)
EXIT{full}
MINIMUM{Full(Services), Full(Declarations), Full(Definitions), Full(Object), Full(Position), Full(Context)}
;
CheckVarInport: INPORT OF CheckVarCall {Full(Services), Full(Declarations), Full(Definitions), Full(Object), Full(Position), Full(Context)};
CheckVarOutport: OUTPORT OF CheckVarInport;


-- CheckLoop
-- Procedure to check the branch from the end of the loop to the beginning
-- If the typestate at the end of the loop is higher, 
--    coercions will be inserted at the beginning of the loop
-- If the typestate at the end of the loop is lower or incomparable, then
--    coercions will be inserted at the beginning of the loop 
--    and a flag will be set so that the loop will be checked again
CheckLoopCall: CALLMESSAGE(
  Services: TypestateCheckingServices, 
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Context: TypestateCheckingEnvironment, -- knowledge needed to check clause
         -- and knowledge needed as input to translation phase
  BeginLoopTS: Typestate, -- typestate at beginning of loop
  EndLoopTS: Typestate, -- typestate at end of loop
  ReCheck: Boolean, -- returned true if loop will need to be re-checked
  LoopClause: ClauseId -- clause being looped 
)
CONSTANT(Services, Code, Definitions, EndLoopTS, LoopClause)
EXIT{full}
MINIMUM {full(Services), full(Code), full(Definitions), full(Context), full(BeginLoopTS), full(EndLoopTS), full(LoopClause)};
CheckLoopInport: INPORT OF CheckLoopCall {full(Services), full(Code), full(Definitions), full(Context), full(BeginLoopTS), full(EndLoopTS), full(LoopClause)};
CheckLoopOutport: OUTPORT OF CheckLoopInport;

-- CheckSelector
-- Procedure to typestate check a selector
-- 
CheckSelectorCall: CALLMESSAGE(
  Services: TypestateCheckingServices, 
  Code: Execution_Environment, -- static code of program
  Definitions: Definitions_Modules, -- definitions used by program
  Position: Aposition, -- location of statement (in case error msg is generated)
  Selector: Selector, -- selector being checked
  Table: Objectname, -- table referred to by selector
  CurrentTS: Typestate, -- typestate at statement containing selector
  Context: TypestateCheckingEnvironment -- knowledge needed to check clause
         -- and knowledge needed as input to translation phase
)
CONSTANT(Services, Code, Definitions, Position, Selector, Table, CurrentTS)
EXIT {full}
MINIMUM {full};
CheckSelectorInport: INPORT OF CheckSelectorCall {full};
CheckSelectorOutport: OUTPORT OF CheckSelectorInport;

-- TypeOf
-- Computes the type of an object
TypeOfCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Definitions: Definitions_Modules, -- definitions used by program
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Object: ObjectName, -- object whose type is sought
  Type: TypeName -- type of Object
)
CONSTANT(Services, Declarations, Definitions, Context, Object)
EXIT{full}
MINIMUM {full(Services), full(Declarations), full(Definitions), full(Context), full(Object)};
TypeOfInport: INPORT OF TypeOfCall {full(Services), full(Declarations), full(Definitions), full(Context), full(Object)};
TypeOfOutport: OUTPORT OF TypeOfInport;

-- Substitute
-- Procedure to create an actual typestate from a formal typestate by subtituting
-- an object name
SubstituteCall: CALLMESSAGE (
  Services: TypestateCheckingServices,
  Object: Objectname, -- object being substituted into the formal typestate
  FormalTypestate: Formal_Typestate, -- the formal typestate
  ActualTypestate: Typestate -- the result after substitution
  )
CONSTANT(Services, Object, FormalTypestate)
EXIT{full};
SubstituteInport: INPORT OF SubstituteCall {full(Services), full(Object), full(FormalTypestate)};
SubstituteOutport: OUTPORT OF SubstituteInport;

-- SubstituteCallParameters
-- Procedure to create an actual typestate from a formal typestate by subtituting
-- a set of actual parameter operands
SubstituteCallParametersCall: CALLMESSAGE (
  Services: TypestateCheckingServices,
  Operands : Objectnames, -- the operand list of a CALL statement
  CallmessageComponents: Component_Declarations, -- from the definition of the callmessage type
  FormalTypestate: Formal_Typestate, -- the formal typestate
  ActualTypestate: Typestate -- the result after substitution
  )
CONSTANT(Services, Operands, CallmessageComponents, FormalTypestate)
EXIT{full};
SubstituteCallParametersInport: INPORT OF SubstituteCallParametersCall {full(Services), full(Operands), full(CallmessageComponents), full(FormalTypestate)};
SubstituteCallParametersOutport: OUTPORT OF SubstituteCallParametersInport;



-- AddDropSets
AddDropSets: TABLE OF LabelledAddDropSet  {full} KEYS(Exceptionname);

LabelledAddDropSet: RECORD(
  ExceptionName: Handlername, -- possible outcome of an operation
  AddDropSet: AddDropSet -- typestate changes
  );
  
AddDropSet: RECORD(
  Adds: Typestate, -- set of attributes added
  Drops: Typestate -- set of attributes dropped
);

-- procedure to merge typestates at join points
-- and to determine what attributes must be dropped by soft coercions at target
SoftGLBCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Definitions: Definitions_Modules, -- definitions used by program
  CurrentTS: Typestate,
  TargetLevel: ScopeOffset, -- offset in Context.Scopes of the scope in which target lies
  TargetTS: OptCoercionInfo)
CONSTANT(Services, Declarations, Context, Definitions, CurrentTS, TargetLevel)
EXIT{full}
MINIMUM{full};
SoftGLBInport: INPORT OF SoftGLBCall {full};
SoftGLBOutport: OUTPORT OF SoftGLBInport;

SoftCoerceCall: CALLMESSAGE(
  Services: TypestateCheckingServices,
  Declarations: Scopes, -- meanings of root object names
  Context: TypestateCheckingEnvironment, -- typestate "knowledge base"
  Definitions: Definitions_Modules, -- definitions used by program
  Drops: Typestate, -- attributes being dropped
  Coercions: Statements -- operations list
)
CONSTANT(Services, Declarations, Context, Definitions) EXIT{full}
MINIMUM {full(Services), full(Declarations), full(Context), full(Definitions), full(Drops)};
SoftCoerceInport: INPORT OF SoftCoerceCall {full(Services), full(Declarations), full(Context), full(Definitions), full(Drops)};
SoftCoerceOutport: OUTPORT OF SoftCoerceInport;

OptCoercionInfo: VARIANT OF option(
  'absent' -> NeverBranched: empty {}, -- the target was never branched to
  'present' -> Branched: CoercionInfo {full}
  );
CoercionInfo: RECORD (
  TargetTS: Typestate, -- GLB of ts from all branch points
  Drops: Typestate -- attributes which must be dropped 
);
SoftCoercionSet: TABLE OF SoftCoercion {full} keys(ClauseId);
SoftCoercion: RECORD (
  ClauseId: clauseid, -- of exception handler
  Dataflow: OptCoercionInfo -- typestate and softcoercions
);

-- TypestateCheckingEnvironment
-- The environment consists of three parts:
-- 1. Path: This consists of information about the blocks enclosing
--    the clause being checked.  This information is thrown away when
--    typestate checking is complete.
-- 2. Inferred Declarations:  Since checking doesn't update the program,
--    any declarations "added" by typechecking go into this auxiliary structure.
-- 3. Knowledge: This consists of information gathered by typestate checking
--    and passed on to the translator.  It is in turn broken down as follows:
--    (a) Inserted Coercions: Coercions added to satisfy preconditions,
--        or to lower typestates at end of a clause.
--    (b) Handler Typestates: Typestates at exception join points
--    (c) Branches: Typestates at source of branches to exceptions
--    Inserted coercions are translated into explicit operations.
--    The other information is used to create "soft" coercions.
--    Information is built "optimistically" -- that is,
--    we assume each pass through a clause will be the last pass.
--    If we have assumed wrong, (a) and (c) are recomputed;
--    (b) can be used to reduce the need to re-scan clauses.
-- 4. Error messages
TypestateCheckingEnvironment: RECORD (
  Scopes: ScopeString, -- list of active scopes, outer to inner
  ExpressionBlocks: ExpressionBlockDescriptors,  -- list of active expression blocks, outer to inner
  HandlerScopes: BlockDescriptors,  -- list of blocks, inner to outer, of which we are in the main clause, and whose handlers are therefore in scope
  Constants: RootnameList, -- list of root objects which are constant (on constant list, or constant by context)
  Inspecting: RootnameList,  -- list of root objects which are Inspecting
  Pos: RootnameList,  -- list of root objects which are POS
  InferredDcls: InferredDefinitions, -- declarations inferred by typechecking
  PreCoercions: CoercionSet, -- coercions before a statement   
  PostCoercions: CoercionSet, -- coercions at the ends of clauses
  HandlerCoercions: SoftCoercionSet, -- soft coercions at the beginnings of handlers
  OuterOthers: Statements, -- soft coercions if process is terminated with an exception
  ErrorMessages: Errors, -- typestate errors detected by checker
  DefinitionsMap: Definitions_PrintMappings, -- information on how to print messages for definitions
  ExecutableMap: Executable_PrintMap -- information on how to print messages for this executable module
);

-- We keep track of all scopes in the path, outer to inner
ScopeString: ORDERED TABLE OF ScopeId {full};

-- We keep track of expression blocks, because within an expression block,
-- all rootnames declared outside that block are constant, except 
-- the expression block result
ExpressionBlockDescriptors:  ORDERED TABLE OF ExpressionBlockDescriptor {full};
ExpressionBlockDescriptor: RECORD (
  Scope: ScopeOffset, -- offset in TypestateCheckingEnvironment.Scopes of the scope
  Result: Rootname -- root name of result 
);
ScopeOffset: integer;  -- offsets in ScopeString lists

-- The block descriptors define the handlers currently in scope, and their typestates
BlockDescriptors: ORDERED TABLE OF BlockDescriptor {full};

BlockDescriptor: RECORD(
  Handlers: Handlers, -- the handlers of the block in scope
  Level: ScopeOffset -- the offset in Scopes of the scope
  );

RootnameList: ORDERED TABLE OF Rootname {full};

-- Services available to Typestate Checking
TypestateCheckingServices: RECORD (
  CheckClause: CheckClauseOutport, 
  ApplyPrecondition: ApplyPreconditionOutport, -- check required attrs present, and forbidden can be coerced
  ApplyPostcondition: ApplyPostconditionOutport, -- check adds/drops produce possible TS
  AttemptToCoerce: AttemptToCoerceOutport, -- obtain coercion and preconditions for dropping an attribute
  Involving: InvolvingOutport, -- obtain attributes to drop to reach given typestate
  ExceptionBranch: ExceptionBranchOutport, -- record a branch
  CheckGuardClause: CheckGuardClauseOutport, -- check that the clause returns an INIT result
  BeginAlternatives: BeginAlternativesOutport, -- typestate check BLOCK, SELECT, and IF
  SoftGLB: SoftGLBOutport, -- compute the GLB at a merge point
  SoftCoerce: SoftCoerceOutport, -- compute the soft coercions given a set of dropped attributes
  ImpliedAttribute: ImpliedAttributeOutport, -- determine whether a missing attribute is implied by current typestate
  CheckVar: CheckVarOutport, -- check that an object is VAR
  CheckLoop: CheckLoopOutport, -- typestate check WHILE, FOR INSPECT, and WHERE clauses
  TypeOf: TypeOfOutport, -- get the type of an object
  Substitute: SubstituteOutport, -- substitute an actual object name for a formal typestate
  SubstituteCallParameters: SubstituteCallParametersOutport,-- substitute the operand list of a call into the formal typestate for its interface
  Checking_Table: Checking_Table, -- pre and post condition rules
  PreconditionFunctions: PreconditionFunctions, -- functions which determine the required and forbidden attributes
  PostconditionRegularFunctions: PostconditionFunctions, -- functions which determine the add and drop sets for normal postcondition, default empty add-drop sets for exceptions
  DetermineCallPostcondition: DetermineCallPostconditionOutport, -- function to determine add/drop sets for call (different from others because of non-trivial exception outcomes, var args)
  Debug: AbsFormat!Formatters, -- debugging routines
  Outside: Stdenv -- I/O operations
  
  );
  
PreconditionFunctions: TABLE OF LabelledPreconditionFunction {full} KEYS(Name);

LabelledPreconditionFunction: RECORD (
  Name: Precondition_Function_Name,
  Function: DeterminePreconditionOutport);
  
PostconditionFunctions: TABLE OF LabelledPostconditionFunction {full} KEYS(Name);

LabelledPostconditionFunction: RECORD (
  Name: PostconditionFunctionName,
  Function: DeterminePostconditionOutport); 

end definitions
