From 0db227de23d77aa5f2c3ff33b3f8fdc1b38270ac Mon Sep 17 00:00:00 2001 From: Saikat Chakraborty Date: Thu, 17 Oct 2024 09:19:42 -0700 Subject: [PATCH] First cut of printing pulse checker dataset. In `Pulse.Main.fst` the function `print_st_typing` prints the proof tree of a function. In the `Pulse.Checker.fst` the `dataset_print` function prints the environment, precondition, statement and postcondition for every pulse query. --- DatasetDump/analyze.ipynb | 340 +++++++++++++++++++++++++++++++ DatasetDump/dump.sh | 5 + src/checker/Pulse.Checker.fst | 95 ++++++--- src/checker/Pulse.Main.fst | 364 +++++++++++++++++++++++++++++++++- 4 files changed, 768 insertions(+), 36 deletions(-) create mode 100644 DatasetDump/analyze.ipynb create mode 100755 DatasetDump/dump.sh diff --git a/DatasetDump/analyze.ipynb b/DatasetDump/analyze.ipynb new file mode 100644 index 000000000..2b6d14db6 --- /dev/null +++ b/DatasetDump/analyze.ipynb @@ -0,0 +1,340 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import json \n", + "import os\n", + "import sys" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "import re\n", + "from typing import Dict, Any\n", + "\n", + "def parse_source_file(range_str: str) -> Dict[str, Any]:\n", + " pattern = r\"^(.*)\\((\\d+),(\\d+)-(\\d+),(\\d+)\\)$\"\n", + " match = re.match(pattern, range_str)\n", + " \n", + " if match:\n", + " file_path = match.group(1)\n", + " start_line = int(match.group(2))\n", + " start_col = int(match.group(3))\n", + " end_line = int(match.group(4))\n", + " end_col = int(match.group(5))\n", + " \n", + " return {\n", + " \"file_path\": file_path,\n", + " \"position\": {\n", + " \"start_line\": start_line,\n", + " \"start_col\": start_col,\n", + " \"end_line\": end_line,\n", + " \"end_col\": end_col\n", + " }\n", + " }\n", + " else:\n", + " raise ValueError(\"Invalid range string format\")\n", + " " + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [], + "source": [ + "dump_logs = [\n", + " l[len(\"TAC>> DATASET \"):].strip()\n", + " for l in open(\"dump.dataset.log\").readlines() if l.startswith(\"TAC>> DATASET \")\n", + "]" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "application/vnd.jupyter.widget-view+json": { + "model_id": "e04df9e7f74f4f2496296fc462a53a45", + "version_major": 2, + "version_minor": 0 + }, + "text/plain": [ + " 0%| | 0/6900 [00:00= other.end_col\n", + " return self.start_line <= other.start_line and self.end_line >= other.end_line\n", + " \n", + " def add_child(self, child_node):\n", + " for c in self.children:\n", + " if c.is_my_decendent(child_node):\n", + " c.add_child(child_node)\n", + " return\n", + " self.children.append(child_node)\n", + " child_node.parent = self\n", + " \n", + " def __str__(self):\n", + " statement = json.dumps((self.data_point['statement'][:30] + '...') if len(self.data_point['statement']) > 30 else self.data_point['statement'])\n", + " precond = json.dumps(' -> '.join(self.data_point['preconditions'])[:30] + '...') if len(';'.join(self.data_point['preconditions'])) > 30 else ';'.join(self.data_point['preconditions'])\n", + " postcod = json.dumps((str(self.data_point['postcondition'])[:30] + '...') if len(str(self.data_point['postcondition'])) > 30 else str(self.data_point['postcondition']))\n", + " return f\"{'✓' if self.source_presence else '✕'} {self.data_point['type_of_statement']} \" +\\\n", + " f\"({self.start_line},{self.start_col})-({self.end_line},{self.end_col}) : {statement} -> {precond} -> {postcod}\"\n", + " \n", + " def prettyPrint(self, indent=0):\n", + " print(\"|--\" * indent + str(self))\n", + " for c in self.children:\n", + " c.prettyPrint(indent+1)\n", + " \n", + " \n", + " def size(self):\n", + " return 1 + sum([c.size() for c in self.children])\n", + " \n", + " " + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Node 0: 14 ✓ totbind (57,2)-(63,4) : \"let (contents: _) = Pulse.Lib....\" -> \"pure (FStar.SizeT.fits (2 * FS...\" -> \"(exists* (pht:Pulse.Lib.HashTa...\"\n", + "Node 1: 4 ✓ proofhintwithbinders (75,10)-(76,15) : \"unfold Pulse.Lib.HashTable.mod...\" -> \"(exists* (pht:Pulse.Lib.HashTa...\" -> \"emp\"\n", + "Node 2: 2 ✓ return (77,2)-(77,20) : \"Pulse.Lib.Vec.free (contents h...\" -> \"Pulse.Lib.Vec.pts_to ht.conten...\" -> \"emp\"\n", + "Node 3: 118 ✓ totbind (100,2)-(196,5) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "Node 4: 47 ✓ totbind (217,2)-(241,3) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "Node 5: 193 ✓ totbind (262,2)-(413,3) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"(exists* (pht':Pulse.Lib.HashT...\"\n", + "Node 6: 55 ✓ totbind (438,2)-(489,3) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "Node 7: 17 ✓ totbind (510,2)-(520,3) : \"let (b: _) = Pulse.Lib.HashTab...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"(exists* (pht':Pulse.Lib.HashT...\"\n", + "Node 8: 110 ✓ totbind (539,2)-(634,3) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"(exists* (pht':Pulse.Lib.HashT...\"\n" + ] + } + ], + "source": [ + "nodes = []\n", + "for didx in node_id_to_dataset:\n", + " d = node_id_to_dataset[didx]\n", + " if d[\"file_path\"] != \"lib/Pulse.Lib.HashTable.fst\":\n", + " continue\n", + " d = node_id_to_dataset[didx]\n", + " n = Node(didx)\n", + " if len(nodes) == 0:\n", + " nodes.append(n)\n", + " else:\n", + " for node in nodes:\n", + " if node.is_my_decendent(n):\n", + " node.add_child(n)\n", + " break\n", + " else:\n", + " nodes.append(n)\n", + " \n", + "for nidx, n in enumerate(nodes):\n", + " print(f\"Node {nidx}: \", n.size(), n)" + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "✓ totbind (217,2)-(241,3) : \"let (hashf: _) = hashf ht;\\nlet...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--✕ return (217,14)-(217,22) : \"hashf ht\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"\"\n", + "|--✓ withlocal (218,2)-(241,3) : \"let mut (contents: _) = conten...\" -> \"pure (hashf == ht.hashf) -> Pu...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--✓ proofhintwithbinders (218,33)-(219,15) : \"unfold Pulse.Lib.HashTable.mod...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--✕ proofhintwithbinders (218,33)-(219,15) : \"with (?kt:\\nPrims.eqtype)\\n(?vt:...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--✕ bind (218,33)-(219,15) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--✕ rewrite (218,33)-(219,15) : \"rewrite\\nPulse.Lib.HashTable.mo...\" -> \"Pulse.Lib.HashTable.models ht ...\" -> \"\"\n", + "|--|--✓ proofhintwithbinders (219,16)-(220,92) : \"rewrite Pulse.Lib.Reference.pt...\" -> \"Pulse.Lib.Vec.pts_to ht.conten...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--✓ bind (219,16)-(220,92) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.Vec.pts_to ht.conten...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--✓ rewrite (219,16)-(220,92) : \"rewrite\\nPulse.Lib.Reference.pt...\" -> \"Pulse.Lib.Vec.pts_to ht.conten...\" -> \"\"\n", + "|--|--✓ proofhintwithbinders (220,93)-(221,100) : \"rewrite Pulse.Lib.Vec.pts_to (...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--✓ bind (220,93)-(221,100) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--✓ rewrite (220,93)-(221,100) : \"rewrite\\nPulse.Lib.Vec.pts_to (...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"\"\n", + "|--|--✓ totbind (222,2)-(241,3) : \"let (v': _) =\\n Pulse.Lib.Vec....\" -> \"Pulse.Lib.Vec.pts_to (FStar.Gh...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--✓ stapp (222,11)-(222,58) : \"Pulse.Lib.Vec.replace_i_ref co...\" -> \"Pulse.Lib.Vec.pts_to (FStar.Gh...\" -> \"\"\n", + "|--|--|--✓ totbind (223,2)-(241,3) : \"let (vcontents: _) = !contents...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--✓ stapp (223,18)-(223,27) : \"!contents\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"\"\n", + "|--|--|--|--✓ totbind (224,2)-(241,3) : \"let (ht1: _) = Pulse.Lib.HashT...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--✕ return (224,12)-(224,39) : \"Pulse.Lib.HashTable.mk_ht (sz ...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"\"\n", + "|--|--|--|--|--✓ proofhintwithbinders (225,2)-(225,87) : \"with (s: _).rewrite Pulse.Lib....\" -> \"pure (ht1 == Pulse.Lib.HashTab...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✓ proofhintwithbinders (225,2)-(225,87) : \"with (s: _).assert Pulse.Lib.V...\" -> \"Pulse.Lib.Reference.pts_to con...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--✓ bind (225,2)-(225,87) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.Vec.pts_to (FStar.Gh...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--✓ rewrite (225,2)-(225,87) : \"rewrite\\nPulse.Lib.Vec.pts_to (...\" -> \"Pulse.Lib.Vec.pts_to (FStar.Gh...\" -> \"\"\n", + "|--|--|--|--|--✓ proofhintwithbinders (225,88)-(226,48) : \"fold Pulse.Lib.HashTable.model...\" -> \"Pulse.Lib.Vec.pts_to ht1.conte...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✕ bind (225,88)-(226,48) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.Vec.pts_to ht1.conte...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--✕ rewrite (225,88)-(226,48) : \"rewrite\\nPulse.Lib.Vec.pts_to h...\" -> \"Pulse.Lib.Vec.pts_to ht1.conte...\" -> \"\"\n", + "|--|--|--|--|--✓ match (227,2)-(241,3) : \"match v' with\\n{\\n(Pulse.Lib.Has...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✕ proofhintwithbinders (229,6)-(231,9) : \"rewrite each v' as Pulse.Lib.H...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--✕ bind (229,6)-(231,9) : \"let (_: Prims.unit) = rewrite ...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--✕ rewrite (229,6)-(231,9) : \"rewrite emp emp\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"\"\n", + "|--|--|--|--|--|--|--|--|--✓ totbind (229,6)-(231,9) : \"let (res: _) = (ht1 <: Pulse.L...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--|--|--✕ return (229,16)-(229,41) : \"(ht1 <: Pulse.Lib.HashTable.Ty...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"\"\n", + "|--|--|--|--|--|--|--|--|--|--✓ proofhintwithbinders (230,6)-(230,66) : \"with (pht: _).rewrite Pulse.Li...\" -> \"pure (res == ((ht1 <: Pulse.Li...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--|--|--|--✓ proofhintwithbinders (230,6)-(230,66) : \"with (pht: _).assert Pulse.Lib...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--|--|--|--|--✓ bind (230,6)-(230,66) : \"let (_: Prims.unit) =\\n rewrit...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--|--|--|--|--|--✓ rewrite (230,6)-(230,66) : \"rewrite\\nPulse.Lib.HashTable.mo...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"\"\n", + "|--|--|--|--|--|--|--|--|--|--✓ return (231,6)-(231,9) : \"res\" -> \"Pulse.Lib.HashTable.models (FS...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✕ proofhintwithbinders (233,14)-(234,30) : \"rewrite each v' as Pulse.Lib.H...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--✕ bind (233,14)-(234,30) : \"let (_: Prims.unit) = rewrite ...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--✕ rewrite (233,14)-(234,30) : \"rewrite emp emp\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"\"\n", + "|--|--|--|--|--|--|--|--|--✓ proofhintwithbinders (233,14)-(234,30) : \"assert pure (Used? v');\\nunreac...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✓ unreachable (235,6)-(235,35) : \"unreachable ()\" -> \"pure (Used? v') -> Pulse.Lib.H...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✕ proofhintwithbinders (237,15)-(238,30) : \"rewrite each v' as Pulse.Lib.H...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--✕ bind (237,15)-(238,30) : \"let (_: Prims.unit) = rewrite ...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--|--|--✕ rewrite (237,15)-(238,30) : \"rewrite emp emp\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"\"\n", + "|--|--|--|--|--|--|--|--|--✓ proofhintwithbinders (237,15)-(238,30) : \"assert pure (Used? v');\\nunreac...\" -> \"Pulse.Lib.HashTable.models ht1...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n", + "|--|--|--|--|--|--✓ unreachable (239,6)-(239,35) : \"unreachable ()\" -> \"pure (Used? v') -> Pulse.Lib.H...\" -> \"Pulse.Lib.HashTable.models (FS...\"\n" + ] + } + ], + "source": [ + "nodes[4].prettyPrint()" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "popai", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.11.5" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/DatasetDump/dump.sh b/DatasetDump/dump.sh new file mode 100755 index 000000000..989d232e1 --- /dev/null +++ b/DatasetDump/dump.sh @@ -0,0 +1,5 @@ +git clean -fdx lib; + +OTHERFLAGS='--admit_smt_queries true' make -j12 boot-checker; + +OTHERFLAGS='--ext pulse:dataset=1' make -j1 | tee DatasetDump/dump.dataset.log; \ No newline at end of file diff --git a/src/checker/Pulse.Checker.fst b/src/checker/Pulse.Checker.fst index 109adff0b..40df4ed15 100644 --- a/src/checker/Pulse.Checker.fst +++ b/src/checker/Pulse.Checker.fst @@ -189,34 +189,75 @@ let maybe_trace (t:st_term) (g:env) (pre:term) (rng:range) : T.Tac unit = *) let env_bindings_to_string (g:env) : T.Tac string = String.concat "; " <| - T.map (fun (x, n, t) -> - Printf.sprintf "%s @ %d : %s" - (T.unseal (x <: ppname).name) - (n <: var) - (Stubs.Pprint.render (Syntax.Printer.term_to_doc t))) - (Pulse.Typing.Env.bindings_with_ppname g) + T.map + (fun (x, n, t) -> + Printf.sprintf "%s @ %d : %s" + (T.unseal (x <: ppname).name) + (n <: var) + (Stubs.Pprint.render (Syntax.Printer.term_to_doc t))) + (Pulse.Typing.Env.bindings_with_ppname g) + +let env_bindings_to_json_list (g:env) : T.Tac Pulse.Json.json = + let open Pulse.Json in + JsonList ( + T.map + (fun (x, n, t) -> + JsonAssoc ([ + "name", JsonStr (T.unseal (x <: ppname).name); + "index", JsonInt (n <: var); + "type", JsonStr (Stubs.Pprint.render (Syntax.Printer.term_to_doc t)) + ])) + (Pulse.Typing.Env.bindings_with_ppname g) + ) let print_post_hint (g:env) (p:post_hint_opt g) : T.Tac string = match p with - | None -> "no goal set" - | Some p -> - // print p.post - //use term_to_doc as above - "" - + | None -> "" + | Some p -> Syntax.Printer.term_to_string (p <: post_hint_t).post + +let get_type_of_statement (t:st_term) : string = + match t.term with + | Tm_Return _ -> "return" + | Tm_Abs _ -> "abs" + | Tm_STApp _ -> "stapp" + | Tm_ElimExists _ -> "elimexists" + | Tm_IntroExists _ -> "introexists" + | Tm_Bind _ -> "bind" + | Tm_TotBind _ -> "totbind" + | Tm_If _ -> "if" + | Tm_While _ -> "while" + | Tm_Match _ -> "match" + | Tm_ProofHintWithBinders _ -> "proofhintwithbinders" + | Tm_WithLocal _ -> "withlocal" + | Tm_WithLocalArray _ -> "withlocalarray" + | Tm_Par _ -> "par" + | Tm_IntroPure _ -> "intropure" + | Tm_Admit _ -> "admit" + | Tm_Unreachable _ -> "unreachable" + | Tm_Rewrite _ -> "rewrite" + | Tm_WithInv _ -> "withinv" + | _ -> "unknown" + //add post_hint as an argument to dataset_print let dataset_print (g: env) (pre: term) (res_ppname: ppname) (t: st_term) (post_hint:post_hint_opt g) : T.Tac unit = - if T.ext_getv "pulse:dataset" = "1" then - T.print (Printf.sprintf "DATASET %s" (let open Pulse.Json in - let res = Syntax.Pure.slprop_as_list pre in - string_of_json (JsonAssoc ([ - "range", JsonStr (T.range_to_string t.range); - "statement", JsonStr (Stubs.Pprint.render (Syntax.Printer.st_term_to_doc t)); - "environment", JsonStr (env_bindings_to_string g); - //add a field called, say, "goal" - //and set its value to JsonStr of print_post_hint - "resources", JsonList (Tactics.Util.map (fun pre -> JsonStr (Stubs.Pprint.render (Syntax.Printer.term_to_doc pre))) (Syntax.Pure.slprop_as_list pre)); - ])))) + if T.ext_getv "pulse:dataset" = "1" then + T.print ( + Printf.sprintf "DATASET %s" ( + let open Pulse.Json in + let res = Syntax.Pure.slprop_as_list pre in + string_of_json (JsonAssoc ([ + "range", JsonStr (T.range_to_string t.range); + "preconditions", JsonList ( + Tactics.Util.map (fun p -> JsonStr (Syntax.Printer.term_to_string p)) res + ); + "statement", JsonStr (Stubs.Pprint.render (Syntax.Printer.st_term_to_doc t)); + "postcondition", JsonStr (print_post_hint g post_hint); + "environment", env_bindings_to_json_list g; + "type_of_statement", JsonStr (get_type_of_statement t); + "is_in_source", JsonBool (T.unseal t.source); + ])) + ) + ) #push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1" let rec check @@ -228,15 +269,15 @@ let rec check (t:st_term) : T.Tac (checker_result_t g0 pre0 post_hint) = RU.with_error_bound #(checker_result_t g0 pre0 post_hint) t.range <| fun () -> + // let _ = dataset_print g0 pre0 res_ppname t post_hint in if Pulse.Checker.AssertWithBinders.handle_head_immediately t - then Pulse.Checker.AssertWithBinders.check g0 pre0 pre0_typing post_hint res_ppname t check + then + Pulse.Checker.AssertWithBinders.check g0 pre0 pre0_typing post_hint res_ppname t check else ( let (| g, pre, pre_typing, k_elim_pure |) = Pulse.Checker.Prover.elim_exists_and_pure pre0_typing in - maybe_trace t g pre t.range; - if RU.debug_at_level (fstar_env g) "pulse.checker" then T.print (Printf.sprintf "At %s{\nerr context:\n>%s\n\n{\n\tenv=%s\ncontext:\n%s,\n\nst_term: %s}}\n" (T.range_to_string t.range) @@ -245,8 +286,6 @@ let rec check (Pulse.Syntax.Printer.term_to_string pre) (Pulse.Syntax.Printer.st_term_to_string t)); - dataset_print g pre res_ppname t post_hint; - let r : checker_result_t g pre post_hint = let g = push_context (P.tag_of_st_term t) t.range g in match t.term with diff --git a/src/checker/Pulse.Main.fst b/src/checker/Pulse.Main.fst index 92d77f960..64f74d92c 100644 --- a/src/checker/Pulse.Main.fst +++ b/src/checker/Pulse.Main.fst @@ -15,21 +15,369 @@ *) module Pulse.Main - -module T = FStar.Tactics.V2 -module R = FStar.Reflection.V2 -module RT = FStar.Reflection.Typing open FStar.Tactics.V2 - open Pulse.Syntax open Pulse.Typing open Pulse.Checker open Pulse.Elaborate open Pulse.Soundness +module T = FStar.Tactics.V2 +module R = FStar.Reflection.V2 +module RT = FStar.Reflection.Typing module Cfg = Pulse.Config module RU = Pulse.RuntimeUtils module P = Pulse.Syntax.Printer module Rec = Pulse.Recursion +open Pulse.Json + +let env_bindings_to_json (g:env) : T.Tac Pulse.Json.json = + JsonList ( + T.map + (fun (x, n, t) -> + JsonAssoc ([ + "name", JsonStr (T.unseal (x <: ppname).name); + "index", JsonInt (n <: var); + "type", JsonStr (Stubs.Pprint.render (Syntax.Printer.term_to_doc t)) + ])) + (Pulse.Typing.Env.bindings_with_ppname g) + ) + +let qualifier_to_json (q: option qualifier) : T.Tac Pulse.Json.json = + JsonStr(Pulse.Syntax.Printer.qual_to_string q) + +let binder_to_json (b: binder) : T.Tac Pulse.Json.json = + JsonAssoc ([ + "type", JsonStr ""; + "name", JsonStr (T.unseal (b.binder_ppname <: ppname).name); + "attributes", JsonList ( + T.map (fun t -> JsonStr (Pulse.Syntax.Printer.term_to_string t)) (T.unseal b.binder_attrs) + ) + ]) + +#push-options "--z3rlimit_factor 4" +let rec jsonize_st_typing #g #t #c (d:st_typing g t c) : T.Tac Pulse.Json.json = + let open Pulse.Json in + match d with + | T_Abs g x q b u body c total_typing body_typing -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Abs"); + // "environment", env_bindings_to_json g; + // "x", JsonInt (x <: var); + // "q", qualifier_to_json q; + "b", binder_to_json b; + // "universe", JsonStr (Pulse.Syntax.Printer.univ_to_string u); + // "body", JsonStr(Pulse.Syntax.Printer.st_term_to_string body); + // "body_range", JsonStr (T.range_to_string body.range); + // "comp", JsonStr(Pulse.Syntax.Printer.comp_to_string c); + "body", jsonize_st_typing body_typing; + ]) + | T_STApp g head ty q res arg tot_typing_head tot_typing_arg -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_STApp"); + // "environment", env_bindings_to_json g; + // "head", JsonStr(Pulse.Syntax.Printer.term_to_string head); + // "ty", JsonStr(Pulse.Syntax.Printer.term_to_string ty); + // "q", qualifier_to_json q; + // "res", JsonStr(Pulse.Syntax.Printer.comp_to_string res); + // "arg", JsonStr(Pulse.Syntax.Printer.term_to_string arg); + // "tot_typing_head", jsonize_st_typing tot_typing_head; + // "tot_typing_arg", jsonize_st_typing tot_typing_arg; + "stmt", JsonStr (Pulse.Syntax.Printer.st_term_to_string (t)); + "comp", JsonStr (Pulse.Syntax.Printer.comp_to_string (c)); + ]) + | T_STGhostApp g head ty q res arg x ghost_typing_head non_informative ghost_typing_arg -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_STGhostApp"); + "stmt", JsonStr (Pulse.Syntax.Printer.st_term_to_string (t)); + "comp", JsonStr (Pulse.Syntax.Printer.comp_to_string (c)); + // "environment", env_bindings_to_json g; + // "head", JsonStr(Pulse.Syntax.Printer.term_to_string head); + // "ty", JsonStr(Pulse.Syntax.Printer.term_to_string ty); + // "q", qualifier_to_json q; + // "res", JsonStr(Pulse.Syntax.Printer.comp_to_string res); + // "arg", JsonStr(Pulse.Syntax.Printer.term_to_string arg); + // "x", JsonInt (x <: var); + // "ghost_typing_head", jsonize_st_typing ghost_typing_head; + // "non_informative", jsonize_st_typing non_informative; + // "ghost_typing_arg", jsonize_st_typing ghost_typing_arg; + ]) + | T_Return g c use_eq u t e post x tot_typing_e tot_typing_post tot_typing_x -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Return"); + // "environment", env_bindings_to_json g; + // "ctag", JsonStr(Pulse.Syntax.Printer.ctag_to_string c); + // "use_eq", JsonBool use_eq; + // "universe", JsonStr (Pulse.Syntax.Printer.univ_to_string u); + // "type", JsonStr(Pulse.Syntax.Printer.term_to_string t); + "e", JsonStr(Pulse.Syntax.Printer.term_to_string e); + "post", JsonStr(Pulse.Syntax.Printer.term_to_string post); + // "x", JsonInt (x <: var); + // "tot_typing_e", jsonize_st_typing tot_typing_e; + // "tot_typing_post", jsonize_st_typing tot_typing_post; + // "tot_typing_x", jsonize_st_typing tot_typing_x; + ]) + | T_Lift g e c1 c2 d1 comp -> + // JsonAssoc ([ + // "stmt_type", JsonStr ("T_Lift"); + // // "environment", env_bindings_to_json g; + // // "e", JsonStr(Pulse.Syntax.Printer.st_term_to_string e); + // // "e_range", JsonStr (T.range_to_string e.range); + // // "c1", JsonStr(Pulse.Syntax.Printer.comp_to_string c1); + // // "c2", JsonStr(Pulse.Syntax.Printer.comp_to_string c2); + // "d1", jsonize_st_typing d1; + // // "d2", jsonize_st_typing comp; + // ]) + jsonize_st_typing d1 + | T_Bind g e1 e2 c1 c2 b x c d1 total_typing d2 bind_comp -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Bind"); + // "environment", env_bindings_to_json g; + // "e1", JsonStr(Pulse.Syntax.Printer.st_term_to_string e1); + // "e1_range", JsonStr (T.range_to_string e1.range); + // "e2", JsonStr(Pulse.Syntax.Printer.st_term_to_string e2); + // "e2_range", JsonStr (T.range_to_string e2.range); + // "c1", JsonStr(Pulse.Syntax.Printer.comp_to_string c1); + // "c2", JsonStr(Pulse.Syntax.Printer.comp_to_string c2); + // "b", binder_to_json b; + // "x", JsonInt (x <: var); + // "c", JsonStr(Pulse.Syntax.Printer.comp_to_string c); + "d1", jsonize_st_typing d1; + // "total_typing", jsonize_st_typing total_typing; + "d2", jsonize_st_typing d2; + // "bind_comp", jsonize_st_typing bind_comp; + ]) + | T_BindFn g e1 e2 c1 c2 b x d1 ghost_erased_universe total_typing d2 bind_comp -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_BindFn"); + // "environment", env_bindings_to_json g; + // "e1", JsonStr(Pulse.Syntax.Printer.st_term_to_string e1); + // "e1_range", JsonStr (T.range_to_string e1.range); + // "e2", JsonStr(Pulse.Syntax.Printer.st_term_to_string e2); + // "e2_range", JsonStr (T.range_to_string e2.range); + // "c1", JsonStr(Pulse.Syntax.Printer.comp_to_string c1); + // "c2", JsonStr(Pulse.Syntax.Printer.comp_to_string c2); + // "b", binder_to_json b; + // "x", JsonInt (x <: var); + "d1", jsonize_st_typing d1; + // "universe", JsonStr (Pulse.Syntax.Printer.univ_to_string ghost_erased_universe); + // "total_typing", TODO + "d2", jsonize_st_typing d2; + // "bind_comp", JsonStr (Pulse.Syntax.Printer.comp_to_string bind_comp); + ]) + | T_If g b e1 e2 c hyp total_typing e1_st_typing e2_st_typing erased_comp -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_If"); + // "environment", env_bindings_to_json g; + "b", JsonStr(Pulse.Syntax.Printer.term_to_string b); + // "e1", JsonStr(Pulse.Syntax.Printer.st_term_to_string e1); + // "e1_range", JsonStr (T.range_to_string e1.range); + // "e2", JsonStr(Pulse.Syntax.Printer.st_term_to_string e2); + // "e2_range", JsonStr (T.range_to_string e2.range); + // "c", JsonStr(Pulse.Syntax.Printer.comp_to_string c); + // "hyp", JsonStr(Pulse.Syntax.Printer.term_to_string hyp); + // "total_typing", jsonize_st_typing total_typing; + "e1_st_typing", jsonize_st_typing e1_st_typing; + "e2_st_typing", jsonize_st_typing e2_st_typing; + // "erased_comp", jsonize_st_typing erased_comp; + ]) + | T_Match g sc_u sc_ty sc total_typing1 total_typing2 c erased brs brs_typing pats_complt -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Match"); + // "environment", env_bindings_to_json g; + // "sc_u", JsonStr (Pulse.Syntax.Printer.univ_to_string sc_u); + // "sc_ty", JsonStr (Pulse.Syntax.Printer.term_to_string sc_ty); + // "sc", JsonStr (Pulse.Syntax.Printer.term_to_string sc); + // "total_typing1", jsonize_st_typing total_typing1; + // "total_typing2", jsonize_st_typing total_typing2; + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "erased", jsonize_st_typing erased; + // "branches", JsonList( + // T.map (fun (p, e) -> JsonAssoc([ + // "pattern", JsonStr (Pulse.Syntax.Printer.pattern_to_string p); + // "expr", JsonStr (Pulse.Syntax.Printer.st_term_to_string e); + // "expr_range", JsonStr (T.range_to_string (e <: st_term).range); + // ])) brs + // ); + // "brs_typing", jsonize_st_typing brs_typing; // TODO: This is a list of typing derivations for different branchs + // "pats_complt", jsonize_st_typing pats_complt; + ]) + | T_Frame g e comp frame total_typing body -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Frame"); + // "environment", env_bindings_to_json g; + // "e", JsonStr (Pulse.Syntax.Printer.st_term_to_string e); + // "e_range", JsonStr (T.range_to_string e.range); + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + "frame", JsonStr (Pulse.Syntax.Printer.term_to_string frame); + // "total_typing", jsonize_st_typing total_typing; + "body", jsonize_st_typing body; + "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + ]) + | T_Equiv g e c c' d eq -> + // JsonAssoc ([ + // "stmt_type", JsonStr ("T_Equiv"); + // // "environment", env_bindings_to_json g; + // // "e", JsonStr (Pulse.Syntax.Printer.st_term_to_string e); + // // "e_range", JsonStr (T.range_to_string e.range); + // // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // // "c'", JsonStr (Pulse.Syntax.Printer.comp_to_string c'); + // "d", jsonize_st_typing d; + // // "eq", jsonize_st_typing eq; + // ]) + jsonize_st_typing d + | T_Sub g e c c' d sub -> + // JsonAssoc ([ + // "stmt_type", JsonStr ("T_Sub"); + // "environment", env_bindings_to_json g; + // "e", JsonStr (Pulse.Syntax.Printer.st_term_to_string e); + // "e_range", JsonStr (T.range_to_string e.range); + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "c'", JsonStr (Pulse.Syntax.Printer.comp_to_string c'); + // "d", jsonize_st_typing d; + // // "sub", jsonize_st_typing sub; + // ]) + jsonize_st_typing d + | T_IntroPure g p tot_typing prop_validity -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_IntroPure"); + // "environment", env_bindings_to_json g; + "p", JsonStr (Pulse.Syntax.Printer.term_to_string p); + // "tot_typing", jsonize_st_typing tot_typing; + // "prop_validity", jsonize_st_typing prop_validity; + ]) + | T_ElimExists g u t p x tot_typing1 tot_typing2 -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_ElimExists"); + // "environment", env_bindings_to_json g; + // "u", JsonStr (Pulse.Syntax.Printer.univ_to_string u); + "t", JsonStr (Pulse.Syntax.Printer.term_to_string t); + "p", JsonStr (Pulse.Syntax.Printer.term_to_string p); + // "x", JsonInt (x <: var); + // "tot_typing1", jsonize_st_typing tot_typing1; + // "tot_typing2", jsonize_st_typing tot_typing1; + ]) + | T_IntroExists g u b p e tot_typing1 tot_typing2 ghost_typing -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_IntroExists"); + // "environment", env_bindings_to_json g; + // "u", JsonStr (Pulse.Syntax.Printer.univ_to_string u); + // "b", binder_to_json b; + "p", JsonStr (Pulse.Syntax.Printer.term_to_string p); + "e", JsonStr (Pulse.Syntax.Printer.term_to_string e); + // "tot_typing1", jsonize_st_typing tot_typing1; + // "tot_typing2", jsonize_st_typing tot_typing2; + // "ghost_typing", jsonize_st_typing ghost_typing; + ]) + | T_While g inv cond body tot_typing_inv st_typing_cond st_typing_body -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_While"); + // "environment", env_bindings_to_json g; + "inv", JsonStr (Pulse.Syntax.Printer.term_to_string inv); + // "cond", JsonStr (Pulse.Syntax.Printer.st_term_to_string cond); + // "cond_range", JsonStr (T.range_to_string cond.range); + // "body", JsonStr (Pulse.Syntax.Printer.st_term_to_string body); + // "body_range", JsonStr (T.range_to_string body.range); + // "tot_typing_inv", jsonize_st_typing tot_typing_inv; + "st_typing_cond", jsonize_st_typing st_typing_cond; + "st_typing_body", jsonize_st_typing st_typing_body; + ]) + | T_Par g eL cL eR cR x comp_typing_cl comp_typing_cr st_typing_cl st_typing_cr -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Par"); + // "environment", env_bindings_to_json g; + // "eL", JsonStr (Pulse.Syntax.Printer.st_term_to_string eL); + // "eL_range", JsonStr (T.range_to_string eL.range); + // "cL", JsonStr (Pulse.Syntax.Printer.comp_to_string cL); + // "eR", JsonStr (Pulse.Syntax.Printer.st_term_to_string eR); + // "eR_range", JsonStr (T.range_to_string eR.range); + // "cR", JsonStr (Pulse.Syntax.Printer.comp_to_string cR); + // "x", JsonInt (x <: var); + // "comp_typing_cl", jsonize_st_typing comp_typing_cl; + // "comp_typing_cr", jsonize_st_typing comp_typing_cr; + "st_typing_cl", jsonize_st_typing st_typing_cl; + "st_typing_cr", jsonize_st_typing st_typing_cr; + ]) + | T_WithLocal g binder_ppname init body init_t c x tot_typing univerese_of comp_typing_u st_typing -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_WithLocal"); + // "environment", env_bindings_to_json g; + "binder_ppname", JsonStr (T.unseal binder_ppname.name); + "init", JsonStr (Pulse.Syntax.Printer.term_to_string init); + // "body", JsonStr (Pulse.Syntax.Printer.st_term_to_string body); + // "body_range", JsonStr (T.range_to_string body.range); + "init_t", JsonStr (Pulse.Syntax.Printer.term_to_string init_t); + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "x", JsonInt (x <: var); + // "tot_typing", jsonize_st_typing tot_typing; + // "universe_of", JsonStr (Pulse.Syntax.Printer.univ_to_string univerese_of); + // "comp_typing_u", jsonize_st_typing comp_typing_u; + "st_typing", jsonize_st_typing st_typing; + ]) + | T_WithLocalArray g binder_ppname initializer length body a c x tot_typing_initializer tot_typing_length universe_of comp_typing_u st_typing -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_WithLocalArray"); + // "environment", env_bindings_to_json g; + "binder_ppname", JsonStr (T.unseal binder_ppname.name); + "initializer", JsonStr (Pulse.Syntax.Printer.term_to_string initializer); + "length", JsonStr (Pulse.Syntax.Printer.term_to_string length); + // "body", JsonStr (Pulse.Syntax.Printer.st_term_to_string body); + // "body_range", JsonStr (T.range_to_string body.range); + "init_t", JsonStr (Pulse.Syntax.Printer.term_to_string a); + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "x", JsonInt (x <: var); + // "tot_typing_initializer", jsonize_st_typing tot_typing_initializer; + // "tot_typing_length", jsonize_st_typing tot_typing_length; + // "universe_of", JsonStr (Pulse.Syntax.Printer.univ_to_string universe_of); + // "comp_typing_u", jsonize_st_typing comp_typing_u; + "st_typing", jsonize_st_typing st_typing; + ]) + | T_Rewrite g p q tot_typing_p slprop_equiv -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Rewrite"); + // "environment", env_bindings_to_json g; + "p", JsonStr (Pulse.Syntax.Printer.term_to_string p); + "q", JsonStr (Pulse.Syntax.Printer.term_to_string q); + // "tot_typing_p", jsonize_st_typing tot_typing_p; + // "slprop_equiv", jsonize_st_typing slprop_equiv; + ]) + | T_Admit g c comp_typing -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Admit"); + // "environment", env_bindings_to_json g; + "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "comp_typing", jsonize_st_typing comp_typing; + ]) + | T_Unreachable g c comp_typing prop_validity -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_Unreachable"); + // "environment", env_bindings_to_json g; + "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "comp_typing", jsonize_st_typing comp_typing; + // "prop_validity", jsonize_st_typing prop_validity; + ]) + | T_WithInv g i p body c tot_typing_i tot_typing_p body_typing inv_disjointness_token -> + JsonAssoc ([ + "stmt_type", JsonStr ("T_WithInv"); + // "environment", env_bindings_to_json g; + "inv", JsonStr (Pulse.Syntax.Printer.term_to_string i); + "inv_type", JsonStr (Pulse.Syntax.Printer.term_to_string p); + // "body", JsonStr (Pulse.Syntax.Printer.st_term_to_string body); + // "body_range", JsonStr (T.range_to_string body.range); + // "c", JsonStr (Pulse.Syntax.Printer.comp_to_string c); + // "tot_typing_i", jsonize_st_typing tot_typing_i; + // "tot_typing_p", jsonize_st_typing tot_typing_p; + "body_typing", jsonize_st_typing body_typing; + // "inv_disjointness_token", jsonize_st_typing inv_disjointness_token; + ]) + | _ -> JsonStr "" + + + +let print_st_typing #g #t #c (d:st_typing g t c) : T.Tac unit = + let open Pulse.Json in + let json = jsonize_st_typing d in + T.print (string_of_json json) + let debug_main g (s: unit -> T.Tac string) : T.Tac unit = if RU.debug_at_level (fstar_env g) "pulse.main" @@ -59,7 +407,7 @@ let set_impl #g #t (se: RT.sigelt_for g t) (r: bool) (impl: R.term) : Dv (RT.sig let se = RU.add_attribute se (Extract.CompilerLib.mk_extracted_as_attr impl) in checked, se, blob -#push-options "--z3rlimit_factor 4" +#push-options "--z3rlimit_factor 10" let check_fndefn (d : decl{FnDefn? d.d}) (g : Soundness.Common.stt_env{bindings g == []}) @@ -97,9 +445,9 @@ let check_fndefn (fun _ -> Printf.sprintf "\nchecker call returned in main with:\n%s\nderivation=%s\n" (P.st_term_to_string body) (Pulse.Typing.Printer.print_st_typing t_typing)); - - let refl_t = elab_comp c in + let _ = print_st_typing t_typing in + let refl_t = elab_comp c in let refl_e = Pulse.RuntimeUtils.embed_st_term_for_extraction #st_term body (Some rng) in let blob = "pulse", refl_e in soundness_lemma g body c t_typing;