File size: 5,646 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 | #include "cs_test.h"
#include "l4_dissonance.h"
#include <stdio.h>
#include <string.h>
static int handler_calls;
static cs_status handler_last;
static void on_trap(const dis_violation *v, void *ctx)
{
(void)ctx;
handler_calls++;
handler_last = v->code;
}
static int flag_value = 1;
static int flag_inv(void *ctx) { return *(int *)ctx != 0; }
TEST_MAIN_BEGIN("l4 dissonance")
dis_engine e;
dis_init(&e);
dis_set_trap_handler(&e, on_trap, NULL);
/* direct contradiction */
CHECK(dis_value(&e, "p") == -1);
CHECK_EQ_STATUS(dis_assert(&e, "p", 1), CS_OK);
CHECK_EQ_STATUS(dis_assert(&e, "p", 1), CS_OK); /* idempotent */
CHECK(dis_value(&e, "p") == 1);
CHECK(!dis_is_trapped(&e));
CHECK_EQ_STATUS(dis_assert(&e, "p", 0), CS_ERR_CONTRADICTION);
CHECK(dis_is_trapped(&e) && handler_calls == 1 && handler_last == CS_ERR_CONTRADICTION);
CHECK(dis_value(&e, "p") == 1); /* state unchanged */
CHECK(dis_violation_count(&e) == 1);
CHECK(strstr(dis_violation_at(&e, 0)->msg, "'p'") != NULL);
/* trapped: everything refused until reset */
CHECK_EQ_STATUS(dis_assert(&e, "q", 1), CS_ERR_TRAPPED);
CHECK_EQ_STATUS(dis_add_implication(&e, "a", "b"), CS_ERR_TRAPPED);
CHECK_EQ_STATUS(dis_check_invariants(&e), CS_ERR_TRAPPED);
CHECK(dis_value(&e, "q") == -1);
CHECK_EQ_STATUS(dis_reset_trap(&e), CS_OK);
CHECK(!dis_is_trapped(&e) && dis_violation_count(&e) == 1); /* log is kept */
CHECK_EQ_STATUS(dis_assert(&e, "q", 1), CS_OK);
/* implication: modus ponens and modus tollens */
dis_init(&e);
CHECK_EQ_STATUS(dis_add_implication(&e, "a", "b"), CS_OK);
CHECK_EQ_STATUS(dis_add_implication(&e, "b", "c"), CS_OK);
CHECK_EQ_STATUS(dis_assert(&e, "a", 1), CS_OK);
CHECK(dis_value(&e, "b") == 1 && dis_value(&e, "c") == 1); /* transitive chain */
CHECK_EQ_STATUS(dis_assert(&e, "c", 0), CS_ERR_CONTRADICTION); /* derived contradiction */
dis_reset_trap(&e);
CHECK(dis_value(&e, "c") == 1); /* nothing was committed */
dis_init(&e);
dis_add_implication(&e, "a", "b");
dis_add_implication(&e, "b", "c");
CHECK_EQ_STATUS(dis_assert(&e, "c", 0), CS_OK); /* modus tollens */
CHECK(dis_value(&e, "b") == 0 && dis_value(&e, "a") == 0);
CHECK_EQ_STATUS(dis_assert(&e, "a", 1), CS_ERR_CONTRADICTION);
CHECK(dis_value(&e, "a") == 0);
/* unknown stays unknown when the rule does not force it */
dis_init(&e);
dis_add_implication(&e, "a", "b");
CHECK_EQ_STATUS(dis_assert(&e, "a", 0), CS_OK);
CHECK(dis_value(&e, "b") == -1);
CHECK_EQ_STATUS(dis_assert(&e, "b", 1), CS_OK);
CHECK(dis_value(&e, "a") == 0);
/* exclusion */
dis_init(&e);
dis_add_exclusion(&e, "sealed", "mutable");
CHECK_EQ_STATUS(dis_assert(&e, "sealed", 1), CS_OK);
CHECK(dis_value(&e, "mutable") == 0);
CHECK_EQ_STATUS(dis_assert(&e, "mutable", 1), CS_ERR_CONTRADICTION);
dis_init(&e);
dis_add_exclusion(&e, "x", "y");
CHECK_EQ_STATUS(dis_assert(&e, "y", 1), CS_OK);
CHECK(dis_value(&e, "x") == 0); /* symmetric */
/* new rule conflicting with established facts is rejected and not installed */
dis_init(&e);
dis_assert(&e, "a", 1);
dis_assert(&e, "b", 0);
CHECK_EQ_STATUS(dis_add_implication(&e, "a", "b"), CS_ERR_CONTRADICTION);
CHECK(e.nimpl == 0);
dis_reset_trap(&e);
CHECK_EQ_STATUS(dis_add_implication(&e, "b", "a"), CS_OK); /* consistent: b false => a unknown ok */
/* implication cycle behaves as equivalence */
dis_init(&e);
dis_add_implication(&e, "p", "q");
dis_add_implication(&e, "q", "p");
CHECK_EQ_STATUS(dis_assert(&e, "q", 0), CS_OK);
CHECK(dis_value(&e, "p") == 0);
/* invariants */
dis_init(&e);
dis_add_invariant(&e, "flag-set", flag_inv, &flag_value);
CHECK_EQ_STATUS(dis_check_invariants(&e), CS_OK);
flag_value = 0;
CHECK_EQ_STATUS(dis_check_invariants(&e), CS_ERR_CONTRADICTION);
CHECK(dis_is_trapped(&e) && strstr(dis_violation_at(&e, 0)->msg, "flag-set") != NULL);
flag_value = 1;
/* explicit trap from another layer */
dis_init(&e);
CHECK_EQ_STATUS(dis_trap(&e, CS_ERR_DRIFT, "sigma drift"), CS_ERR_DRIFT);
CHECK(dis_is_trapped(&e));
CHECK(dis_violation_at(&e, 0)->code == CS_ERR_DRIFT);
/* violation ring keeps the newest DIS_MAX_VIOLATIONS in order */
dis_init(&e);
for (int i = 0; i < DIS_MAX_VIOLATIONS + 5; i++) {
char m[16];
snprintf(m, sizeof m, "v%d", i);
dis_trap(&e, CS_ERR_STATE, m);
}
CHECK(dis_violation_count(&e) == DIS_MAX_VIOLATIONS + 5);
CHECK(strcmp(dis_violation_at(&e, 0)->msg, "v5") == 0);
CHECK(strcmp(dis_violation_at(&e, DIS_MAX_VIOLATIONS - 1)->msg, "v20") == 0);
CHECK(dis_violation_at(&e, DIS_MAX_VIOLATIONS) == NULL);
CHECK(dis_violation_at(&e, 0)->seq == 6);
/* argument and capacity checks */
dis_init(&e);
CHECK_EQ_STATUS(dis_assert(&e, "", 1), CS_ERR_ARG);
CHECK_EQ_STATUS(dis_assert(&e, "p", 2), CS_ERR_ARG);
CHECK_EQ_STATUS(dis_assert(NULL, "p", 1), CS_ERR_ARG);
for (int i = 0; i < DIS_MAX_FACTS; i++) {
char n[16];
snprintf(n, sizeof n, "f%d", i);
CHECK_EQ_STATUS(dis_assert(&e, n, 1), CS_OK);
}
CHECK_EQ_STATUS(dis_assert(&e, "overflow", 1), CS_ERR_NOMEM);
CHECK(dis_is_trapped(NULL)); /* NULL engine counts as trapped */
TEST_MAIN_END
|