Maybe found the bug

harmonylang · Mar 20, 2024 · e57cb30 · e57cb30
1 parent bc1a663
commit e57cb30
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 7 deletions.
diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c
@@ -435,7 +435,7 @@ static void process_step(
             f->type = so->failed ? FAIL_SAFETY : FAIL_TERMINATION;
             f->node = node;
             f->edge = walloc_fast(w, sizeof(struct edge));
-#ifdef SHORT_POINTER
+#ifdef SHORT_PTR
             f->edge->dest = (int64_t *) node - (int64_t *) f->edge;
             printf("SET DST 1: %p\n", node);
 #else
@@ -556,7 +556,7 @@ static void process_step(
     struct dict_assoc *hn = dict_find_new(w->visited, &w->allocator,
                 sc, size, noutgoing * sizeof(struct edge), &new, &lock);
     struct node *next = (struct node *) &hn[1];
-#ifdef SHORT_POINTER
+#ifdef SHORT_PTR
     edge->dest = (int64_t *) next - (int64_t *) edge;
     printf("SET DST 2: next=%p edge=%p diff=%ld(%ld,%ld) %p\n", next, edge, (int64_t) edge->dest,
     (int64_t *) next - (int64_t *) edge,
@@ -2904,7 +2904,7 @@ static void worker(void *arg){
                 struct node *root = global.graph.nodes[0];
                 struct edge *re = node_edges(root);
                 struct node *rd = edge_dst(re);
-#ifdef SHORT_POINTER
+#ifdef SHORT_PTR
                 printf("N0: %d %d %p (%ld)\n", (int) root->id, root->nedges, rd, (int64_t) re->dest);
                 printf("N0...: %d %d %p (%d)\n", (int) root->id, root->nedges, rd, (int) rd->id);
 #endif

diff --git a/harmony_model_checker/charm/graph.c b/harmony_model_checker/charm/graph.c
@@ -40,15 +40,15 @@ unsigned int graph_add_multiple(struct graph *graph, unsigned int n) {
     return node_id;
 }
 
-#ifndef notdef
+#ifdef SHORT_PTR
 void dump_edges(struct node *src){
     struct edge *e = node_edges(src);
     for (unsigned int i = 0; i < src->nedges; i++, e++) {
         printf("--> dst=%p(%ld) stc=%u m=%u f=%u\n",
             edge_dst(e), (int64_t) e->dest, e->stc_id, e->multiple, e->failed);
     }
 }
-#endif // notdef
+#endif
 
 struct edge *find_edge(struct node *src, struct node *dst){
     struct edge *e = node_edges(src);

diff --git a/harmony_model_checker/charm/graph.h b/harmony_model_checker/charm/graph.h
@@ -102,7 +102,8 @@ struct step_comp {
 // information of how a program can get from the source state to the destination
 // state.
 struct edge {
-#ifdef SHORT_POINTER
+#ifdef SHORT_PTR
+XYXZZ
     int64_t dest : 37;          // "short" pointer to dst node
     uint32_t stc_id : 25;       // id of step_condition
 #define edge_dst(e)          ((struct node *) ((int64_t *) (e) + (e)->dest))

diff --git a/harmony_model_checker/charm/head.h b/harmony_model_checker/charm/head.h
@@ -1,6 +1,6 @@
 // #define DEBUGGING
 
-// #define SHORT_POINTER
+// #define SHORT_PTR
 
 #ifdef DEBUGGING
 # undef NDEBUG