Fixed path optimization + make '-B' flag optional

Author: rvanren

code/prog4enter.hny

@@ -1,13 +1,13 @@
-shared = 0
+x = 0
 entered = [ False, False ]
 
 def f(self):
     entered[self] = True
     await not entered[1 - self]
-    shared += 1
+    x += 1
     entered[self] = False
 
 spawn f(0)
 spawn f(1)
 
-finally shared == 2
+finally x == 2

harmony_model_checker/charm/charm.c

@@ -835,8 +835,7 @@ static inline void process_step(
         f->edge = edge;
         add_failure(&w->failures, f);
     }
-
-    if (w->dfa != NULL) {
+    else if (w->dfa != NULL) {
         assert(so->nlog == 0 || so->nlog == 1);
         for (unsigned int i = 0; i < so->nlog; i++) {
             int t = dfa_step(w->dfa, sc->dfa_state, step_log(so)[i]);
@@ -1845,7 +1844,7 @@ static void path_recompute(){
         hvalue_t ctx = edge_input(e)->ctx;
 
         // printf("MACRO tid=%u ctx=%p choice=%p\n", macro->tid, (void *) ctx,
-        //    (void *) edge_input(e)->choice);
+        //                                   (void *) edge_input(e)->choice);
 
         if (e->invariant_chk) {
             global.processes = realloc(global.processes, (global.nprocesses + 1) * sizeof(hvalue_t));
@@ -1879,9 +1878,9 @@ static void path_recompute(){
             }
             global.oldpid = pid;
         }
-        // printf("Macrostep %u: T%u -> %p\n", i, pid, (void *) ctx);
+        // printf("Macrostep %u: T%u/%u -> %p\n", i, pid, global.nprocesses, (void *) ctx);
         if (pid >= global.nprocesses) {
-            printf("PID %p %u %u\n", HV_TO_P(ctx), pid, global.nprocesses);
+            // printf("PID %p %u %u\n", HV_TO_P(ctx), pid, global.nprocesses);
             // panic("bad pid");
             global.nmacrosteps = i;
             break;
@@ -2185,6 +2184,11 @@ static bool path_edge_conflict(
     struct edge *edge,
     struct edge *edge2
 ) {
+    // Consider it a conflict if either edge spawns new threads
+    if (edge_output(edge)->nspawned > 0 || edge_output(edge2)->nspawned > 0) {
+        return true;
+    }
+
     for (struct access_info *ai = edge_output(edge)->ai; ai != NULL; ai = ai->next) {
         if (ai->indices != NULL) {
             for (struct access_info *ai2 = edge_output(edge2)->ai; ai2 != NULL; ai2 = ai2->next) {

harmony_model_checker/charm/ops.c

@@ -674,8 +674,14 @@ void op_Print(const void *env, struct state *state, struct step *step){
         if (global.dfa != NULL) {
             int t = dfa_step(global.dfa, state->dfa_state, combo);
             if (t < 0) {
-                char *p = value_string(combo);
-                value_ctx_failure(step->ctx, step->allocator, "Behavior failure on %s", p);
+                char *p;
+                if (attrs == VALUE_DICT) {
+                    p = value_string(symbol);
+                }
+                else {
+                    p = value_string(combo);
+                }
+                value_ctx_failure(step->ctx, step->allocator, "Behavior failure on printing %s", p);
                 free(p);
                 return;
             }

harmony_model_checker/main.py

@@ -119,10 +119,10 @@ def handle_hny(ns, output_files, parse_code_only, filenames):
 
     return code, scope
 
-def handle_hvm(ns, output_files, parse_code_only, code, scope):
+def handle_hvm(ns, output_files, parse_code_only, code, scope, behavior):
     charm_options = ns.cf or []
-    if ns.B:
-        charm_options.append("-B" + ns.B)
+    if behavior != None:
+        charm_options.append("-B" + behavior)
     if ns.b:
         charm_options.append("-b")
     if ns.T:
@@ -175,16 +175,11 @@ def handle_hvm(ns, output_files, parse_code_only, code, scope):
             print("charm model checker failed")
             exit(r)
 
-def handle_hco(ns, output_files):
+def handle_hco(ns, output_files, behavior):
     if ns.quick:
         return
 
     suppress_output = ns.suppress
-
-    behavior = None
-    if ns.B:
-        behavior = ns.B
-
     disable_browser = settings.values.disable_web or ns.noweb
 
     b = Brief()
@@ -270,14 +265,29 @@ def main():
             return 1
         output_files[suffix] = str(p)
 
-    if len(ns.args) != 1:
-        print(f"harmony: error: invalid number of arguments ({len(ns.args)}). Provide 1 argument.")
-        args.print_help()
-        return 1
+    filename = None
+    behavior_file = ns.B if ns.B else None
+    for f in ns.args:
+        name = pathlib.Path(f)
+        if not name.exists():
+            print(f"harmony: error: file named '{name}' does not exist.")
+            return 1
+        file_type = name.suffix
+        if file_type == '.hfa':
+            if behavior_file != None:
+                print(f"harmony: error: duplicate behavior file.")
+                return 1
+            behavior_file = f
+        elif filename == None:
+            filename = name
+        else:
+            print(f"harmony: error: multiple input files.")
+            args.print_help()
+            return 1
 
-    filename = pathlib.Path(ns.args[0])
-    if not filename.exists():
-        print(f"harmony: error: file named '{filename}' does not exist.")
+    if filename == None:
+        print(f"harmony: no input file")
+        args.print_help()
         return 1
 
     stem = str(filename.parent / filename.stem)
@@ -314,17 +324,17 @@ def main():
     if input_file_type == ".hny":
         code, scope = handle_hny(ns, output_files, parse_code_only, str(filename))
         if charm_flag:
-            handle_hvm(ns, output_files, parse_code_only, code, scope)
-            handle_hco(ns, output_files)
+            handle_hvm(ns, output_files, parse_code_only, code, scope, behavior_file)
+            handle_hco(ns, output_files, behavior_file)
         else:
             print("Skipping Phases 2-5...", flush=True)
             legacy_harmony.dumpCode(print_code, code, scope)
 
     if input_file_type == ".hvm":
         print("Skipping Phase 1...", flush=True)
-        handle_hvm(ns, output_files, parse_code_only, None, None)
-        handle_hco(ns, output_files)
+        handle_hvm(ns, output_files, parse_code_only, None, None, behavior_file)
+        handle_hco(ns, output_files, behavior_file)
 
     if input_file_type == ".hco":
         print("Skipping Phases 1-4...", flush=True)
-        handle_hco(ns, output_files)
+        handle_hco(ns, output_files, behavior_file)