From c101c981d4e903297ea7b85584e849907d62a03a Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 14 Jan 2025 13:24:32 +0100 Subject: [PATCH] Use ocamlgraph fork to fix missing rec bug. --- engine/hax-engine.opam | 3 ++ engine/hax-engine.opam.template | 3 ++ .../toolchain__attributes into-fstar.snap | 4 +- .../toolchain__reordering into-coq.snap | 24 ++++++++++ .../toolchain__reordering into-fstar.snap | 12 +++++ .../toolchain__reordering into-ssprove.snap | 44 +++++++++++++++++++ tests/reordering/src/lib.rs | 14 ++++++ 7 files changed, 102 insertions(+), 2 deletions(-) diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam index e317a03f5..56b671995 100644 --- a/engine/hax-engine.opam +++ b/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"] ] \ No newline at end of file diff --git a/engine/hax-engine.opam.template b/engine/hax-engine.opam.template index 43794c9a8..593f86aaa 100644 --- a/engine/hax-engine.opam.template +++ b/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"] ] \ No newline at end of file diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 8705e5981..9eb7c82e7 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/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*" ''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index d3b0567d8..42cbf0bbf 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/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). +''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap index 50d0e39c8..d2d516b69 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap +++ b/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" diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap index b6655f747..e0130182c 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap +++ b/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. +''' diff --git a/tests/reordering/src/lib.rs b/tests/reordering/src/lib.rs index 03e4d0ea8..fb03140e2 100644 --- a/tests/reordering/src/lib.rs +++ b/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() + } +}