File size: 6,075 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 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 | #include "l4_dissonance.h"
#include <stdio.h>
#include <string.h>
void dis_init(dis_engine *e)
{
memset(e, 0, sizeof *e);
}
void dis_set_trap_handler(dis_engine *e, dis_trap_fn fn, void *ctx)
{
e->on_trap = fn;
e->trap_ctx = ctx;
}
static int name_ok(const char *n)
{
return n && n[0] != '\0' && strlen(n) < DIS_NAME_MAX;
}
static int find_fact(const dis_engine *e, const char *name)
{
for (size_t i = 0; i < e->nfacts; i++)
if (strcmp(e->fact_name[i], name) == 0) return (int)i;
return -1;
}
static int intern(dis_engine *e, const char *name)
{
int i = find_fact(e, name);
if (i >= 0) return i;
if (e->nfacts == DIS_MAX_FACTS) return -1;
strcpy(e->fact_name[e->nfacts], name);
e->fact_value[e->nfacts] = -1;
return (int)e->nfacts++;
}
cs_status dis_trap(dis_engine *e, cs_status code, const char *msg)
{
if (!e) return CS_ERR_ARG;
dis_violation *v = &e->log[e->nviolations % DIS_MAX_VIOLATIONS];
v->seq = ++e->seq;
v->code = code;
snprintf(v->msg, sizeof v->msg, "%s", msg ? msg : "");
e->nviolations++;
e->trapped = 1;
if (e->on_trap) e->on_trap(v, e->trap_ctx);
return code;
}
/* Propagates over a scratch copy of the values. Returns the index of a fact involved in a
* contradiction, or -1 if consistent. */
static int propagate(const dis_engine *e, int8_t *val)
{
int changed = 1;
while (changed) {
changed = 0;
for (size_t r = 0; r < e->nimpl; r++) {
size_t a = e->impl[r].a, b = e->impl[r].b;
if (val[a] == 1) {
if (val[b] == 0) return (int)b;
if (val[b] == -1) { val[b] = 1; changed = 1; }
}
if (val[b] == 0) { /* modus tollens */
if (val[a] == 1) return (int)a;
if (val[a] == -1) { val[a] = 0; changed = 1; }
}
}
for (size_t r = 0; r < e->nexcl; r++) {
size_t a = e->excl[r].a, b = e->excl[r].b;
if (val[a] == 1) {
if (val[b] == 1) return (int)b;
if (val[b] == -1) { val[b] = 0; changed = 1; }
}
if (val[b] == 1) {
if (val[a] == 1) return (int)a;
if (val[a] == -1) { val[a] = 0; changed = 1; }
}
}
}
return -1;
}
static cs_status contradiction(dis_engine *e, int fact, const char *what)
{
char msg[DIS_MSG_MAX];
snprintf(msg, sizeof msg, "contradiction on '%s': %s", e->fact_name[fact], what);
return dis_trap(e, CS_ERR_CONTRADICTION, msg);
}
cs_status dis_assert(dis_engine *e, const char *name, int value)
{
if (!e || !name_ok(name) || (value != 0 && value != 1)) return CS_ERR_ARG;
if (e->trapped) return CS_ERR_TRAPPED;
int f = intern(e, name);
if (f < 0) return CS_ERR_NOMEM;
if (e->fact_value[f] == (int8_t)(1 - value)) return contradiction(e, f, "opposite value already established");
int8_t scratch[DIS_MAX_FACTS];
memcpy(scratch, e->fact_value, sizeof scratch);
scratch[f] = (int8_t)value;
int bad = propagate(e, scratch);
if (bad >= 0) return contradiction(e, bad, "derived from rules");
memcpy(e->fact_value, scratch, sizeof scratch); /* commit atomically */
return CS_OK;
}
int dis_value(const dis_engine *e, const char *name)
{
int f = (e && name) ? find_fact(e, name) : -1;
return f < 0 ? -1 : e->fact_value[f];
}
static cs_status add_rule(dis_engine *e, const char *a, const char *b, int exclusion)
{
if (!e || !name_ok(a) || !name_ok(b)) return CS_ERR_ARG;
if (e->trapped) return CS_ERR_TRAPPED;
size_t *n = exclusion ? &e->nexcl : &e->nimpl;
if (*n == DIS_MAX_RULES) return CS_ERR_NOMEM;
int ia = intern(e, a), ib = intern(e, b);
if (ia < 0 || ib < 0) return CS_ERR_NOMEM;
if (exclusion) { e->excl[*n].a = (size_t)ia; e->excl[*n].b = (size_t)ib; }
else { e->impl[*n].a = (size_t)ia; e->impl[*n].b = (size_t)ib; }
(*n)++;
/* the new rule must be consistent with what is already established */
int8_t scratch[DIS_MAX_FACTS];
memcpy(scratch, e->fact_value, sizeof scratch);
int bad = propagate(e, scratch);
if (bad >= 0) {
(*n)--; /* reject the rule */
return contradiction(e, bad, "new rule conflicts with established facts");
}
memcpy(e->fact_value, scratch, sizeof scratch);
return CS_OK;
}
cs_status dis_add_implication(dis_engine *e, const char *a, const char *b) { return add_rule(e, a, b, 0); }
cs_status dis_add_exclusion(dis_engine *e, const char *a, const char *b) { return add_rule(e, a, b, 1); }
cs_status dis_add_invariant(dis_engine *e, const char *name, dis_invariant_fn fn, void *ctx)
{
if (!e || !name_ok(name) || !fn) return CS_ERR_ARG;
if (e->ninv == DIS_MAX_INVARIANTS) return CS_ERR_NOMEM;
strcpy(e->inv[e->ninv].name, name);
e->inv[e->ninv].fn = fn;
e->inv[e->ninv].ctx = ctx;
e->ninv++;
return CS_OK;
}
cs_status dis_check_invariants(dis_engine *e)
{
if (!e) return CS_ERR_ARG;
if (e->trapped) return CS_ERR_TRAPPED;
for (size_t i = 0; i < e->ninv; i++) {
if (!e->inv[i].fn(e->inv[i].ctx)) {
char msg[DIS_MSG_MAX];
snprintf(msg, sizeof msg, "invariant '%s' violated", e->inv[i].name);
return dis_trap(e, CS_ERR_CONTRADICTION, msg);
}
}
return CS_OK;
}
int dis_is_trapped(const dis_engine *e) { return e ? e->trapped : 1; }
cs_status dis_reset_trap(dis_engine *e)
{
if (!e) return CS_ERR_ARG;
e->trapped = 0;
return CS_OK;
}
size_t dis_violation_count(const dis_engine *e) { return e ? e->nviolations : 0; }
const dis_violation *dis_violation_at(const dis_engine *e, size_t i)
{
if (!e) return NULL;
size_t retained = e->nviolations < DIS_MAX_VIOLATIONS ? e->nviolations : DIS_MAX_VIOLATIONS;
if (i >= retained) return NULL;
size_t first = e->nviolations - retained;
return &e->log[(first + i) % DIS_MAX_VIOLATIONS];
}
|