annotationaction.h

   1 #ifndef _ANNOTATIONACTION_H
   2 #define _ANNOTATIONACTION_H
   3
   4 // Annotation type definition
   5 enum anno_type {PotentialCommitPoint, CommitPointDefine, CommitPointDefineCheck,
   6         HBConditionCheck, InterfaceID, InterfaceCond, InterfaceCheck,
   7         InterfacePostCheck}
   8
   9 typedef struct cond_args {
  10         int arg_num;
  11         void* arg_ptrs[];
  12 } cond_args_t;
  13
  14 /**
  15         This class abstracts the execution of the condition check for the
  16         happpens-before relationship. For example, PutIfMatch(__RET__ != NULL) ->
  17         Get. The "__RET__ != NULL" here is the HB condition.
  18 */
  19 class HBConditionExecutor {
  20         public:
  21         HBConditionExecutor(void *_func_ptr, void **_args) :
  22                 func_ptr(_func_ptr),
  23                 args(_args)
  24         {
  25         }
  26
  27         virtual bool execute() = 0;
  28
  29         private:
  30         void *func_ptr;
  31         cond_args_t args;
  32 };
  33
  34 // Function pointers that abstract ID, condition, checks and actions of the
  35 // interface to be done by the model checker internally
  36 typedef (uint64_t) (*interface_ID_t)();
  37 typedef (bool) (*interface_cond_t)();
  38 typedef (void) (*interface_action_t)();
  39
  40 class InterfaceAction {
  41         public:
  42         interface_ID_t getIDAction();
  43         interface_cond_t getCondAction();
  44         // If the returned action is NULL, it means no need for checking!!
  45         interface_action_t getCheckAction();
  46         interface_action_t getPostCheckAction();
  47         private:
  48 }
  49
  50 #endif