model0116.tmpl

[% PROCESS rerouter.tmpl ~%]

before: file ("$this")
{
#include <verifier/rcv.h>

extern void ldv_irq_disable_inc( void );
extern void ldv_irq_disable_dec( void );

#include <linux/kernel.h>
#include <linux/spinlock.h>

extern void __ldv_check_all(spinlock_t *lock);
extern void __ldv_check_interrupt(spinlock_t *lock);


[% # Generate model function prototypes.
   FOREACH sign = signs; PROCESS make_human_sign %]
extern void ldv_lock_in_process[% sign_id %](void);
extern void ldv_lock_in_interrupt[% sign_id %](void);
[% END %]

}


around: define( local_irq_disable() )
{
   ldv_irq_disable_inc()
}

around: define( local_irq_enable() )
{
   ldv_irq_disable_dec()
}

around: define( local_irq_save(flags) )
{
   ldv_irq_disable_inc()
}

around: define( local_irq_restore(flags) )
{
   ldv_irq_disable_dec()
}

around: call( static inline void spin_unlock_irqrestore(..) )
{
   ldv_irq_disable_dec();
}

around: call( static inline void spin_unlock_irq(..) )
{
   ldv_irq_disable_dec();
}

around: call( static inline void spin_lock(..) )
       || call( static inline void spin_lock_bh(..) )
{
   ldv_lock_in_interrupt[% arg_sign(1) %]();
   ldv_lock_in_process[% arg_sign(1) %]();
}

around: call( static inline void spin_lock_irq(..) )
{
   ldv_lock_in_interrupt[% arg_sign(1) %]();
   ldv_irq_disable_inc();
}

around: call( static inline int spin_trylock(..) )
       || call( static inline int spin_trylock_bh(..) )
{
   if ( ldv_undef_int() > 0 ) {
      ldv_lock_in_interrupt[% arg_sign(1) %]();
      ldv_lock_in_process[% arg_sign(1) %]();
      return 1;
   } else {
      return 0;
   }
}

around: call( static inline int spin_trylock_irq(..) )
{
   if ( ldv_undef_int() > 0 ) {
      ldv_lock_in_interrupt[% arg_sign(1) %]();
      ldv_irq_disable_inc();
      return 1;
   } else {
      return 0;
   }
}

after: call( void __ldv_check_all(..) )
{
   ldv_lock_in_interrupt[% arg_sign(1) %]();
   ldv_lock_in_process[% arg_sign(1) %]();
}

after: call( void __ldv_check_interrupt(..) )
{
   ldv_lock_in_interrupt[% arg_sign(1) %]();
}

around: define( spin_lock_irqsave(lock, flags) )
{
   ({
      __ldv_check_interrupt(lock);
      ldv_irq_disable_inc();
   })
}

around: define( spin_lock_irqsave_nested(lock, flags, subclass) )
{
   ({
      __ldv_check_interrupt(lock);
      ldv_irq_disable_inc();
   })
}

around: define( spin_lock_nest_lock(lock, nest_lock) )
{
   __ldv_check_all(lock)
}

around: define( spin_lock_nested(lock, subclass) )
{
   __ldv_check_all(lock)
}

around: define( spin_trylock_irqsave(lock, flags) )
{
   ({
      if ( ldv_undef_int() > 0 ) {
         __ldv_check_interrupt(lock);
         ldv_irq_disable_inc();
         1;
      } else {
         0;
      }
   })
}

around: define( atomic_dec_and_lock(atomic, lock) )
{
   ({
      --atomic;
      if ( atomic == 0 ) {
         __ldv_check_all(lock);
         1;
      } else {
         0;
      }
   })
}

new: file(LDV_COMMON_MODEL)
{

#include <verifier/rcv.h>

extern int LDV_IN_INTERRUPT;

/* LDV_COMMENT_MODEL_STATE Indicates whether interrupts disabled or enabled.*/
int ldv_irq_disable_nesting = 0;

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_irq_disable_inc') Entry in irq_disable/irq_enable section.*/
void
ldv_irq_disable_inc( void )
{
   /* LDV_COMMENT_CHANGE_STATE Increments the level of irq_disable nesting.*/
   ++ldv_irq_disable_nesting;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_irq_disable_dec') Exit from irq_disable/irq_enable section.*/
void
ldv_irq_disable_dec( void )
{
   /* LDV_COMMENT_CHANGE_STATE Decrements the level of irq_disable nesting.*/
   --ldv_irq_disable_nesting;
}

[% # Generate model state variables and functions.
   FOREACH sign = signs; PROCESS make_human_sign %]
static int ldv_lock_in_process_flag[% sign_id %];
static int ldv_lock_in_interrupt_flag[% sign_id %];

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_lock_in_interrupt[% sign_id %]') Checks for interrupt context.*/
void ldv_lock_in_interrupt[% sign_id %](void)
{
   if ( LDV_IN_INTERRUPT == 2 ) {
      /* LDV_COMMENT_CHANGE_STATE usage of the lock in interrupt context.*/
      ++ldv_lock_in_interrupt_flag[% sign_id %];
   }
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_lock_in_process[% sign_id %]') Checks for process context.*/
void ldv_lock_in_process[% sign_id %](void)
{
   if ( ( LDV_IN_INTERRUPT == 1 ) && ( ldv_irq_disable_nesting <= 0 ) ) {
      /* LDV_COMMENT_CHANGE_STATE usage of the lock in process context with enabled interrupts.*/
      ++ldv_lock_in_process_flag[% sign_id %];
   }
}

[% END %]

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_check_final_state') Checks for usage of the same lock in different contexts.*/
void ldv_check_final_state(void)
{
   [% # Initialize all model state variables at the beginning.
      FOREACH sign = signs; PROCESS make_human_sign %]
   /* LDV_COMMENT_ASSERT If you use same lock in interrupt context (e.g. interrupt handler) and in process context, then in the latter case interrupts (maybe just one line) should be disabled.*/
   ldv_assert( ( ldv_lock_in_interrupt_flag[% sign_id %] == 0 ) ||  ( ldv_lock_in_process_flag[% sign_id%] == 0 ) );
   [% END %]
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_initialize') Initialization of lock variables.*/
void ldv_initialize(void)
{
   [% # Initialize all model state variables at the beginning.
      FOREACH sign = signs; PROCESS make_human_sign %]
   ldv_lock_in_process_flag[% sign_id %] = 0;
   ldv_lock_in_interrupt_flag[% sign_id %] = 0;
   [% END %]
}

}