Merge pull request #1228 from cryspen/fix-missing-rec

fix(engine) Use ocamlgraph fork to fix missing rec bug.

engine/default.nix

@@ -1,24 +1,16 @@
-{
-  ocamlPackages,
-  fetchzip,
-  hax-rust-frontend,
-  hax-engine-names-extract,
-  rustc,
-  nodejs,
-  jq,
-  closurecompiler,
-  gnused,
-  lib,
-  removeReferencesTo,
-}: let
+{ ocamlPackages, fetchzip, hax-rust-frontend, hax-engine-names-extract, rustc
+, nodejs, jq, closurecompiler, gnused, lib, removeReferencesTo, fetchFromGitHub
+}:
+let
   non_empty_list = ocamlPackages.buildDunePackage rec {
     pname = "non_empty_list";
     version = "0.1";
     src = fetchzip {
-      url = "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
+      url =
+        "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
       sha256 = "sha256-BJlEi0yG2DRT5vuU9ulucMD5MPFt9duWgcNO1YsigiA=";
     };
-    buildInputs = with ocamlPackages; [base ppxlib ppx_deriving];
+    buildInputs = with ocamlPackages; [ base ppxlib ppx_deriving ];
     duneVersion = "3";
     minimalOCamlVersion = "4.08";
     doCheck = false;
@@ -28,13 +20,12 @@
     version = "0.1";
 
     src = fetchzip {
-      url = "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
+      url =
+        "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
       sha256 = "sha256-nAmWF8MgW0odKkRiFcHGsvJyIxNHaZpnOlNPsef89Fo=";
     };
 
-    buildInputs = [
-      ocamlPackages.ppxlib
-    ];
+    buildInputs = [ ocamlPackages.ppxlib ];
     duneVersion = "3";
     minimalOCamlVersion = "4.04";
     doCheck = false;
@@ -43,7 +34,17 @@
     pname = "hax-engine";
     version = "0.0.1";
     duneVersion = "3";
-    src = lib.sourceFilesBySuffices ./. [".ml" ".mli" ".js" "dune" "dune-js" "dune-project" "sh" "rs" "mld"];
+    src = lib.sourceFilesBySuffices ./. [
+      ".ml"
+      ".mli"
+      ".js"
+      "dune"
+      "dune-js"
+      "dune-project"
+      "sh"
+      "rs"
+      "mld"
+    ];
     buildInputs = with ocamlPackages;
       [
         base
@@ -65,18 +66,17 @@
         stdio
         re
         js_of_ocaml
-        ocamlgraph
-      ]
-      ++
+        (ocamlgraph.overrideAttrs (_: {
+          src = fetchFromGitHub {
+            owner = "maximebuyse";
+            repo = "ocamlgraph";
+            rev = "fix-stable-topological-sort";
+            sha256 = "sha256-l7v7Kxjaz3xP6T91peAzloyusxpsIOYHXLIiiRHa490=";
+          };
+        }))
+      ] ++
       # F* dependencies
-      [
-        batteries
-        menhirLib
-        ppx_deriving
-        ppxlib
-        sedlex
-        stdint
-      ];
+      [ batteries menhirLib ppx_deriving ppxlib sedlex stdint ];
     nativeBuildInputs = [
       rustc
       hax-rust-frontend
@@ -92,23 +92,19 @@
       find "$bin" -type f -exec remove-references-to -t ${ocamlPackages.ocaml} '{}' +
     '';
 
-    outputs = ["out" "bin" "lib"];
+    outputs = [ "out" "bin" "lib" ];
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";
-        nativeBuildInputs =
-          old.nativeBuildInputs
-          ++ [
-            ocamlPackages.odoc
-          ];
-        buildPhase = ''dune build @doc'';
+        nativeBuildInputs = old.nativeBuildInputs ++ [ ocamlPackages.odoc ];
+        buildPhase = "dune build @doc";
         installPhase = "cp -rf _build/default/_doc/_html $out";
-        outputs = ["out"];
+        outputs = [ "out" ];
       });
       js = hax-engine.overrideAttrs (old: {
         name = "hax-engine.js";
-        nativeBuildInputs = old.nativeBuildInputs ++ [closurecompiler gnused];
-        outputs = ["out"];
+        nativeBuildInputs = old.nativeBuildInputs ++ [ closurecompiler gnused ];
+        outputs = [ "out" ];
         buildPhase = ''
           # Enable JS build
           sed -i "s/; (include dune-js)/(include dune-js)/g" bin/dune
@@ -125,5 +121,4 @@
       });
     };
   };
-in
-  hax-engine.overrideAttrs (_: {name = "hax-engine";})
+in hax-engine.overrideAttrs (_: { name = "hax-engine"; })

engine/hax-engine.opam

@@ -59,4 +59,7 @@ build: [
 dev-repo: "git+https://github.com/hacspec/hax.git"
 depexts: [
   ["nodejs"] {}
+]
+pin-depends: [
+  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
 ]

engine/hax-engine.opam.template

@@ -1,3 +1,6 @@
 depexts: [
   ["nodejs"] {}
+]
+pin-depends: [
+  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
 ]

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -516,6 +516,8 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+unfold let some_function _ = "hello from F*"
+
 let before_inlined_code = "example before"
 
 let inlined_code (foo: t_Foo) : Prims.unit =
@@ -528,6 +530,4 @@ let inlined_code (foo: t_Foo) : Prims.unit =
   ()
 
 let inlined_code_after = "example after"
-
-unfold let some_function _ = "hello from F*"
 '''

test-harness/src/snapshots/toolchain__reordering into-coq.snap

@@ -67,6 +67,8 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
 
 (* NotImplementedYet *)
 
+(* NotImplementedYet *)
+
 Definition f (_ : t_u32) : t_Foo :=
   Foo_A.
 
@@ -79,3 +81,25 @@ Definition no_dependency_1_ (_ : unit) : unit :=
 Definition no_dependency_2_ (_ : unit) : unit :=
   tt.
 '''
+"Reordering_Mut_rec.v" = '''
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Definition f (_ : unit) : unit :=
+  g (tt).
+
+Definition g (_ : unit) : unit :=
+  f (tt).
+
+Definition ff_2_ (_ : unit) : unit :=
+  f (tt).
+'''

test-harness/src/snapshots/toolchain__reordering into-fstar.snap

@@ -26,6 +26,18 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Reordering.Mut_rec.fst" = '''
+module Reordering.Mut_rec
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let rec f (_: Prims.unit) : Prims.unit = g ()
+
+and g (_: Prims.unit) : Prims.unit = f ()
+
+let ff_2_ (_: Prims.unit) : Prims.unit = f ()
+'''
 "Reordering.fst" = '''
 module Reordering
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

test-harness/src/snapshots/toolchain__reordering into-ssprove.snap

@@ -92,6 +92,8 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
   f _  :=
     Foo_A : both L1 I1 t_Foo.
@@ -112,3 +114,45 @@ Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1
     solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 '''
+"Reordering_Mut_rec.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  f _  :=
+    solve_lift (g (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  g _  :=
+    solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations ff_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  ff_2_ _  :=
+    solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+'''

tests/reordering/src/lib.rs

@@ -17,3 +17,17 @@ enum Foo {
     A,
     B,
 }
+
+mod mut_rec {
+    fn f() {
+        g()
+    }
+
+    fn f_2() {
+        f()
+    }
+
+    fn g() {
+        f()
+    }
+}