File size: 2,876 Bytes
2166d7e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 | #ifndef L4_DISSONANCE_H
#define L4_DISSONANCE_H
/* Layer 4 - Dissonance engine: contradiction detection and violation trapping.
*
* Facts are named propositions (true / false / unknown). Implication rules (a => b) and exclusion
* rules (not both) are propagated by modus ponens and modus tollens. An assertion is applied
* atomically: if it would create a contradiction nothing changes, the violation is recorded and
* the engine traps. A trapped engine refuses further assertions until dis_reset_trap(). */
#include <stddef.h>
#include <stdint.h>
#include "cs_status.h"
#define DIS_NAME_MAX 48
#define DIS_MAX_FACTS 64
#define DIS_MAX_RULES 64
#define DIS_MAX_INVARIANTS 16
#define DIS_MAX_VIOLATIONS 16
#define DIS_MSG_MAX 96
typedef struct dis_violation {
uint64_t seq;
cs_status code;
char msg[DIS_MSG_MAX];
} dis_violation;
typedef int (*dis_invariant_fn)(void *ctx); /* nonzero = holds */
typedef void (*dis_trap_fn)(const dis_violation *v, void *ctx);
typedef struct dis_engine {
char fact_name[DIS_MAX_FACTS][DIS_NAME_MAX];
int8_t fact_value[DIS_MAX_FACTS]; /* 1 true, 0 false, -1 unknown */
size_t nfacts;
struct { size_t a, b; } impl[DIS_MAX_RULES];
size_t nimpl;
struct { size_t a, b; } excl[DIS_MAX_RULES];
size_t nexcl;
struct { char name[DIS_NAME_MAX]; dis_invariant_fn fn; void *ctx; } inv[DIS_MAX_INVARIANTS];
size_t ninv;
dis_violation log[DIS_MAX_VIOLATIONS]; /* ring */
size_t nviolations; /* total ever recorded */
uint64_t seq;
int trapped;
dis_trap_fn on_trap;
void *trap_ctx;
} dis_engine;
void dis_init(dis_engine *e);
void dis_set_trap_handler(dis_engine *e, dis_trap_fn fn, void *ctx);
cs_status dis_add_implication(dis_engine *e, const char *a, const char *b);
cs_status dis_add_exclusion(dis_engine *e, const char *a, const char *b);
cs_status dis_assert(dis_engine *e, const char *name, int value);
int dis_value(const dis_engine *e, const char *name); /* 1 / 0 / -1 */
cs_status dis_add_invariant(dis_engine *e, const char *name, dis_invariant_fn fn, void *ctx);
cs_status dis_check_invariants(dis_engine *e);
/* Explicit violation trap (used by other layers). Always sets the trapped flag. */
cs_status dis_trap(dis_engine *e, cs_status code, const char *msg);
int dis_is_trapped(const dis_engine *e);
cs_status dis_reset_trap(dis_engine *e); /* keeps facts and the log */
size_t dis_violation_count(const dis_engine *e); /* total recorded */
/* i = 0 is the oldest retained violation; NULL if out of range. */
const dis_violation *dis_violation_at(const dis_engine *e, size_t i);
#endif
|