Add hooks for counting stats

count_stats.py

+#!/usr/bin/env python3
+import sys
+import re
+import json
+import subprocess
+import shutil
+
+if len(sys.argv) < 2:
+    print("Usage: {} <files.c> ...".format(sys.argv[0]))
+    exit(1)
+
+FILES=sys.argv[1:]
+
+for f in FILES:
+    tmpname = f + ".statstmp"
+    shutil.copyfile(f, tmpname)
+    with open(f, "a") as fd:
+        fd.write("//@rc::import enable_debug from refinedc.typing.automation\n")
+
+    o = subprocess.check_output(["./build.sh", f], stderr=subprocess.STDOUT).split(b"\n")
+    results = []
+    total = { "evars": 0, "sideconds": 0, "unsolvedsideconds": 0, "extensible": 0 }
+    current = None
+    def finish():
+        if current is None:
+            return
+        results.append(current)
+    for line in o:
+        if b"coqc " in line:
+            finish()
+            current = { "name" : line.decode("utf8"),
+                        "evars": 0, "sideconds": 0, "unsolvedsideconds": 0, "extensible": 0 }
+        if line == b"EVAR":
+            current["evars"] += 1
+            total["evars"] += 1
+        if line == b"SIDECOND":
+            current["sideconds"] += 1
+            total["sideconds"] += 1
+        if line == b"UNSOLVEDSIDECOND":
+            current["unsolvedsideconds"] += 1
+            total["unsolvedsideconds"] += 1
+        if line == b"EXTENSIBLE":
+            current["extensible"] += 1
+            total["extensible"] += 1
+    finish()
+    print((json.dumps(results, indent=2)))
+    print((json.dumps(total, indent=2)))
+    shutil.move(tmpname, f)

examples/proofs/btree/generated_proof_btree_member.v

@@ -38,7 +38,7 @@ Section proof_btree_member.
       all: print_typesystem_goal "btree_member" "#0".
     - repeat liRStep; liShow.
       all: print_typesystem_goal "btree_member" "#1".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     + unfold btree_invariant in *; by solve_goal.
     + rewrite H1; by apply: (btree_invariant_in_keys_not_None H2).
     + by rewrite list_insert_id.

examples/proofs/btree/generated_proof_free_btree.v

@@ -23,7 +23,7 @@ Section proof_free_btree.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "free_btree" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "free_btree".
   Qed.
 End proof_free_btree.

examples/proofs/btree/generated_proof_key_index.v

@@ -32,7 +32,7 @@ Section proof_key_index.
       all: print_typesystem_goal "key_index" "#0".
     - repeat liRStep; liShow.
       all: print_typesystem_goal "key_index" "#1".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     + destruct (decide (i = s)); by naive_solver lia.
     + move: (elem_of_list_lookup_1 _ _ H14) => [i Hi]. destruct (decide (y = k)); [ done | exfalso ]. assert (k < y) as Hky by lia. assert (i < s)%nat as Hle by by eapply StronglySorted_lookup_index_lt. assert (i < s) as His  by lia. assert (k < k) by by eapply H0. by lia.
     + apply StronglySorted_insert_drop_take; last done. * move => z Hz. destruct (l !! z) eqn:?; naive_solver lia. * move: (elem_of_list_lookup_2 l s y H7) => Hy. rewrite H7 /=.   assert (k ≠ y); [ by set_solver | by lia ].

examples/proofs/btree/generated_proof_new_btree.v

@@ -22,7 +22,7 @@ Section proof_new_btree.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "new_btree" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "new_btree".
   Qed.
 End proof_new_btree.

examples/proofs/latch/generated_proof_latch_release.v

@@ -20,7 +20,7 @@ Section proof_latch_release.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "latch_release" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "latch_release".
   Qed.
 End proof_latch_release.

examples/proofs/latch/generated_proof_latch_wait.v

@@ -25,7 +25,7 @@ Section proof_latch_wait.
       all: print_typesystem_goal "latch_wait" "#0".
     - repeat liRStep; liShow.
       all: print_typesystem_goal "latch_wait" "#1".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "latch_wait".
   Qed.
 End proof_latch_wait.

examples/proofs/lock/generated_proof_increment.v

@@ -23,7 +23,7 @@ Section proof_increment.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "increment" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "increment".
   Qed.
 End proof_increment.

examples/proofs/lock/generated_proof_init.v

@@ -22,7 +22,7 @@ Section proof_init.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "init" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "init".
   Qed.
 End proof_init.

examples/proofs/lock/generated_proof_read_locked.v

@@ -23,7 +23,7 @@ Section proof_read_locked.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "read_locked" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "read_locked".
   Qed.
 End proof_read_locked.

examples/proofs/lock/generated_proof_read_outside.v

@@ -21,7 +21,7 @@ Section proof_read_outside.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "read_outside" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "read_outside".
   Qed.
 End proof_read_outside.

examples/proofs/lock/generated_proof_write_locked.v

@@ -23,7 +23,7 @@ Section proof_write_locked.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "write_locked" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "write_locked".
   Qed.
 End proof_write_locked.

examples/proofs/lock/generated_proof_write_outside.v

@@ -21,7 +21,7 @@ Section proof_write_outside.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "write_outside" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "write_outside".
   Qed.
 End proof_write_outside.

examples/proofs/malloc1/generated_proof_slab_alloc.v

@@ -19,7 +19,7 @@ Section proof_slab_alloc.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "slab_alloc" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "slab_alloc".
   Qed.
 End proof_slab_alloc.

examples/proofs/malloc1/generated_proof_slab_free.v

@@ -19,7 +19,7 @@ Section proof_slab_free.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "slab_free" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "slab_free".
   Qed.
 End proof_slab_free.

examples/proofs/malloc1/generated_proof_slab_init.v

@@ -19,7 +19,7 @@ Section proof_slab_init.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "slab_init" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "slab_init".
   Qed.
 End proof_slab_init.

examples/proofs/mpool/generated_proof_mpool_add_chunk.v

@@ -23,7 +23,7 @@ Section proof_mpool_add_chunk.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "mpool_add_chunk" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by destruct m => //=; solve_goal.
     all: print_sidecondition_goal "mpool_add_chunk".
   Qed.

examples/proofs/mpool/generated_proof_mpool_alloc.v

@@ -32,7 +32,7 @@ Section proof_mpool_alloc.
       all: print_typesystem_goal "mpool_alloc" "#0".
     - repeat liRStep; liShow.
       all: print_typesystem_goal "mpool_alloc" "#2".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "mpool_alloc".
   Qed.
 End proof_mpool_alloc.

examples/proofs/mpool/generated_proof_mpool_alloc_contiguous.v

@@ -35,7 +35,7 @@ Section proof_mpool_alloc_contiguous.
       all: print_typesystem_goal "mpool_alloc_contiguous" "#0".
     - repeat liRStep; liShow.
       all: print_typesystem_goal "mpool_alloc_contiguous" "#2".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: print_sidecondition_goal "mpool_alloc_contiguous".
   Qed.
 End proof_mpool_alloc_contiguous.

examples/proofs/mpool/generated_proof_mpool_alloc_contiguous_no_fallback.v

@@ -43,7 +43,7 @@ Section proof_mpool_alloc_contiguous_no_fallback.
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
       all: print_typesystem_goal "mpool_alloc_contiguous_no_fallback" "#0".
-    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
     all: try by destruct o'; solve_goal.
     all: try by apply mult_le_compat_r; solve_goal.
     all: try by repeat progress rewrite /ly_size/=; have : (x4 - Z.to_nat o' - count > 0)%nat; solve_goal.