From 558f2f4aba3d88c7828d1e9342ba16b5983f21de Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Mon, 18 Dec 2023 16:15:41 -0600 Subject: [PATCH] double check counting info Signed-off-by: Xudong Sun --- tools/gen-t1-t2-lines.py | 192 +++++++++++++++++---------------------- 1 file changed, 85 insertions(+), 107 deletions(-) diff --git a/tools/gen-t1-t2-lines.py b/tools/gen-t1-t2-lines.py index 04b50f27d..853ac3b6f 100644 --- a/tools/gen-t1-t2-lines.py +++ b/tools/gen-t1-t2-lines.py @@ -2,156 +2,134 @@ import json -def main(): - os.system( - "python3 count-lines.py $VERUS_DIR/source/tools/line_count/zookeeper_table zookeeper" - ) - os.system( - "python3 count-lines.py $VERUS_DIR/source/tools/line_count/rabbitmq_table rabbitmq" - ) - os.system( - "python3 count-lines.py $VERUS_DIR/source/tools/line_count/fluent_table fluent" - ) +def count_total_lines(data): + lines = 0 + for key in data: + for inner_key in data[key]: + lines += data[key][inner_key] + return lines + + +def gen_for_controller(controller): os.system( - "python3 count-anvil-lines.py $VERUS_DIR/source/tools/line_count/lib_table" - ) - zk_data = json.load(open("zookeeper-lines.json")) - rmq_data = json.load(open("rabbitmq-lines.json")) - fb_data = json.load(open("fluent-lines.json")) - anvil_data = json.load(open("anvil-lines.json")) - print("ZooKeeper:") - print( - "Liveness & {} & -- & {}".format( - zk_data["liveness_theorem"]["Trusted"], - zk_data["liveness_proof"]["Proof"], - ) - ) - print( - "Conformance & 5 & -- & {}".format( - zk_data["reconcile_impl"]["Proof"] - 5, - ) - ) - print( - "Controller model & -- & -- & {}".format( - zk_data["reconcile_model"]["Proof"], - ) - ) - print( - "Controller impl & -- & {} & --".format( - zk_data["reconcile_model"]["Exec"] + zk_data["reconcile_impl"]["Exec"], - ) - ) - print( - "Trusted wrapper & {} & -- & --".format( - zk_data["wrapper"]["Trusted"], - ) - ) - print( - "Trusted ZooKeeper API & {} & -- & --".format( - zk_data["external_model"]["Trusted"], - ) - ) - print( - "Trusted entry point & {} & -- & --".format( - zk_data["entry"]["Trusted"], + "python3 count-lines.py $VERUS_DIR/source/tools/line_count/{}_table {}".format( + controller, controller ) ) + data = json.load(open("{}-lines.json".format(controller))) + + total_lines = count_total_lines(data) + total_lines -= data["liveness_inv"]["Proof"] - print("RabbitMQ:") + print("{}:".format(controller)) print( "Liveness & {} & -- & {}".format( - rmq_data["liveness_theorem"]["Trusted"], - rmq_data["liveness_proof"]["Proof"], + data["liveness_theorem"]["Trusted"], + data["liveness_proof"]["Proof"], ) ) - print( - "Safety & {} & -- & {}".format( - rmq_data["safety_theorem"]["Trusted"], - rmq_data["safety_proof"]["Proof"], + total_lines -= data["liveness_theorem"]["Trusted"] + total_lines -= data["liveness_proof"]["Proof"] + + if controller == "rabbitmq": + print( + "Safety & {} & -- & {}".format( + data["safety_theorem"]["Trusted"], + data["safety_proof"]["Proof"], + ) + ) + total_lines -= data["safety_theorem"]["Trusted"] + total_lines -= data["safety_proof"]["Proof"] + + if controller == "fluent": + print( + "Conformance & 10 & -- & {}".format( + data["reconcile_impl"]["Proof"] - 10, + ) ) - ) - print( - "Conformance & 5 & -- & {}".format( - rmq_data["reconcile_impl"]["Proof"] - 5, + else: + print( + "Conformance & 5 & -- & {}".format( + data["reconcile_impl"]["Proof"] - 5, + ) ) - ) + total_lines -= data["reconcile_impl"]["Proof"] print( "Controller model & -- & -- & {}".format( - rmq_data["reconcile_model"]["Proof"], + data["reconcile_model"]["Proof"], ) ) + total_lines -= data["reconcile_model"]["Proof"] print( "Controller impl & -- & {} & --".format( - rmq_data["reconcile_model"]["Exec"] + rmq_data["reconcile_impl"]["Exec"], + data["reconcile_model"]["Exec"] + data["reconcile_impl"]["Exec"], ) ) + total_lines -= data["reconcile_model"]["Exec"] + data["reconcile_impl"]["Exec"] print( "Trusted wrapper & {} & -- & --".format( - rmq_data["wrapper"]["Trusted"], + data["wrapper"]["Trusted"], ) ) + total_lines -= data["wrapper"]["Trusted"] + if controller == "zookeeper": + print( + "Trusted ZooKeeper API & {} & -- & --".format( + data["external_model"]["Trusted"], + ) + ) + total_lines -= data["external_model"]["Trusted"] print( "Trusted entry point & {} & -- & --".format( - rmq_data["entry"]["Trusted"], + data["entry"]["Trusted"], ) ) + total_lines -= data["entry"]["Trusted"] + print("{} lines are not included".format(total_lines)) - print("Fluent:") - print( - "Liveness & {} & -- & {}".format( - fb_data["liveness_theorem"]["Trusted"], - fb_data["liveness_proof"]["Proof"], - ) - ) - print( - "Conformance & 10 & -- & {}".format( - fb_data["reconcile_impl"]["Proof"] - 10, - ) - ) - print( - "Controller model & -- & -- & {}".format( - fb_data["reconcile_model"]["Proof"], - ) - ) - print( - "Controller impl & -- & {} & --".format( - fb_data["reconcile_model"]["Exec"] + fb_data["reconcile_impl"]["Exec"], - ) + +def main(): + gen_for_controller("zookeeper") + gen_for_controller("rabbitmq") + gen_for_controller("fluent") + + os.system( + "python3 count-anvil-lines.py $VERUS_DIR/source/tools/line_count/lib_table" ) + anvil_data = json.load(open("anvil-lines.json")) + total_lines = count_total_lines(anvil_data) + total_lines -= anvil_data["test_lines"]["Exec"] + print("Anvil:") print( - "Trusted wrapper & {} & -- & --".format( - fb_data["wrapper"]["Trusted"], + "Lemmas & -- & -- & {}".format( + anvil_data["k8s_lemma_lines"]["Proof"] + + anvil_data["tla_lemma_lines"]["Proof"] ) ) - print( - "Trusted entry point & {} & -- & --".format( - fb_data["entry"]["Trusted"], - ) + total_lines -= ( + anvil_data["k8s_lemma_lines"]["Proof"] + anvil_data["tla_lemma_lines"]["Proof"] ) - print("Anvil:") print( "TLA embedding & {} & -- & --".format( anvil_data["tla_embedding_lines"]["Trusted"] ) ) + total_lines -= anvil_data["tla_embedding_lines"]["Trusted"] + print("Model & {} & -- & --".format(anvil_data["other_lines"]["Trusted"])) + total_lines -= anvil_data["other_lines"]["Trusted"] print( - "Model & {} & -- & --".format( - anvil_data["other_lines"]["Trusted"] - + anvil_data["object_model_lines"]["Trusted"] - ) - ) - print( - "Lemmas & -- & -- & {}".format( - anvil_data["k8s_lemma_lines"]["Proof"] - + anvil_data["tla_lemma_lines"]["Proof"] - ) + "Object view & {} & -- & --".format(anvil_data["object_model_lines"]["Trusted"]) ) + total_lines -= anvil_data["object_model_lines"]["Trusted"] print( - "Shim layer & {} & -- & --".format( + "Object wrapper & {} & -- & --".format( anvil_data["object_wrapper_lines"]["Trusted"] - + anvil_data["other_lines"]["Exec"] ) ) + total_lines -= anvil_data["object_wrapper_lines"]["Trusted"] + print("Shim layer & {} & -- & --".format(anvil_data["other_lines"]["Exec"])) + total_lines -= anvil_data["other_lines"]["Exec"] + print("{} lines are not included".format(total_lines)) if __name__ == "__main__":