Skip to content

Commit

Permalink
Merge branch 'areitz/quarantinev3'
Browse files Browse the repository at this point in the history
  • Loading branch information
Antonin Reitz committed Feb 1, 2024
2 parents 412a91d + 258ea29 commit 04bf0ad
Show file tree
Hide file tree
Showing 56 changed files with 4,913 additions and 2,007 deletions.
19 changes: 19 additions & 0 deletions c/memory.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,15 @@ void mmap_strict_trap (uint8_t* ptr, size_t len) {
return;
}

// syscall wrapper
void mmap_strict_untrap (uint8_t* ptr, size_t len) {
void* p = mmap((void*) ptr, len, PROT_READ|PROT_WRITE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_FIXED, -1, 0);
if (p == MAP_FAILED && errno != ENOMEM) {
fatal_error("non-ENOMEM mmap failure");
}
return;
}

// syscall wrapper
void mmap_trap (uint8_t* ptr, size_t len) {
int r = madvise((void*) ptr, len, MADV_DONTNEED);
Expand All @@ -60,6 +69,11 @@ void mmap_trap (uint8_t* ptr, size_t len) {
return;
}

// wrapper
void mmap_untrap (uint8_t* ptr, size_t len) {
return;
}

// monomorphised functions

// large allocator allocation wrapper
Expand Down Expand Up @@ -87,6 +101,11 @@ size_t *mmap_ptr_us_init() {
return (size_t*) mmap_init(sizeof(size_t));
}

// slabs allocator init
size_t *mmap_array_us_init(size_t len) {
return (size_t*) mmap_init(len * sizeof(size_t));
}

// slabs allocator init
size_class* mmap_sc_init(size_t len) {
return (size_class*) mmap_init(len * sizeof(size_class));
Expand Down
6 changes: 5 additions & 1 deletion dist/ArrayList.c
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/*
This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
KaRaMeL invocation: /nix/store/mn868yr5iykh2k562nja8bw870dqgny4-karamel-67b19d9a05f6578aec0b640fcb6e432ff18daa71-home/krml -skip-compilation -fparentheses -tmpdir dist -library Steel.ArrayArith -static-header Steel.ArrayArith -no-prefix Steel.ArrayArith -bundle Steel.SpinLock= -bundle FStar.\*,Steel.\* -bundle StarMalloc=Map.\*,Impl.\*,Spec.\*,Main,Main.Meta,LargeAlloc[rename=StarMalloc] -bundle SlabsCommon,SlabsFree,SlabsAlloc[rename=Slabs] -bundle SlotsFree,SlotsAlloc[rename=Slots] -bundle ArrayList,ArrayListGen[rename=ArrayList] -no-prefix Main -no-prefix LargeAlloc -no-prefix Mman -no-prefix MemoryTrap -warn-error +9 -add-include Steel_SpinLock:"steel_types.h" -add-include Steel_SpinLock:"steel_base.h" obj/prims.krml obj/FStar_Pervasives_Native.krml obj/FStar_Pervasives.krml obj/FStar_Mul.krml obj/FStar_Squash.krml obj/FStar_Classical.krml obj/FStar_Preorder.krml obj/FStar_Sealed.krml obj/FStar_Range.krml obj/FStar_Calc.krml obj/FStar_StrongExcludedMiddle.krml obj/FStar_Classical_Sugar.krml obj/FStar_List_Tot_Base.krml obj/FStar_List_Tot_Properties.krml obj/FStar_List_Tot.krml obj/FStar_Seq_Base.krml obj/FStar_Seq_Properties.krml obj/FStar_Seq.krml obj/FStar_Math_Lib.krml obj/FStar_Math_Lemmas.krml obj/FStar_BitVector.krml obj/FStar_UInt.krml obj/FStar_UInt32.krml obj/FStar_Int.krml obj/FStar_Int16.krml obj/Seq2.krml obj/Bitmap1.krml obj/Bitmap2.krml obj/FStar_UInt64.krml obj/Bitmap3.krml obj/Bitmap4.krml obj/FStar_Int64.krml obj/FStar_Int32.krml obj/FStar_Int8.krml obj/FStar_UInt16.krml obj/FStar_UInt8.krml obj/FStar_Int_Cast.krml obj/FStar_Ghost.krml obj/FStar_SizeT.krml obj/SeqUtils.krml obj/FStar_VConfig.krml obj/FStar_Float.krml obj/FStar_Char.krml obj/FStar_Pprint.krml obj/FStar_Issue.krml obj/FStar_TypeChecker_Core.krml obj/FStar_Tactics_Common.krml obj/FStar_Reflection_Types.krml obj/FStar_Tactics_Types.krml obj/FStar_Tactics_Result.krml obj/FStar_Monotonic_Pure.krml obj/FStar_Tactics_Effect.krml obj/FStar_Tactics_Unseal.krml obj/FStar_Sealed_Inhabited.krml obj/FStar_Syntax_Syntax.krml obj/FStar_Reflection_V2_Data.krml obj/FStar_Order.krml obj/FStar_Reflection_V2_Builtins.krml obj/FStar_Reflection_Const.krml obj/FStar_Tactics_V2_Builtins.krml obj/FStar_Tactics_SMT.krml obj/FStar_Tactics_Util.krml obj/FStar_Reflection_V2_Derived.krml obj/FStar_Reflection_V2_Compare.krml obj/FStar_Reflection_V2_Derived_Lemmas.krml obj/FStar_Reflection_V2.krml obj/FStar_Tactics_Visit.krml obj/FStar_Tactics_NamedView.krml obj/FStar_PropositionalExtensionality.krml obj/FStar_Reflection_V1_Data.krml obj/FStar_Reflection_V1_Builtins.krml obj/FStar_Tactics_V1_Builtins.krml obj/FStar_Tactics_Builtins.krml obj/FStar_Tactics_V2_SyntaxCoercions.krml obj/FStar_Tactics_V2_SyntaxHelpers.krml obj/FStar_Reflection_V2_Formula.krml obj/FStar_Tactics_V2_Derived.krml obj/FStar_Tactics_Print.krml obj/FStar_IndefiniteDescription.krml obj/FStar_Reflection_V1_Derived.krml obj/FStar_Reflection_V1_Formula.krml obj/FStar_Reflection_V1_Compare.krml obj/FStar_Reflection_V1_Derived_Lemmas.krml obj/FStar_Reflection_V1.krml obj/FStar_Tactics_V1_SyntaxHelpers.krml obj/FStar_Tactics_V1_Derived.krml obj/FStar_Tactics_V1_Logic.krml obj/FStar_Tactics_V1.krml obj/FStar_Tactics.krml obj/FStar_PtrdiffT.krml obj/FStar_Real.krml obj/Steel_FractionalPermission.krml obj/FStar_Witnessed_Core.krml obj/FStar_MSTTotal.krml obj/FStar_NMSTTotal.krml obj/FStar_PCM.krml obj/Steel_Preorder.krml obj/FStar_FunctionalExtensionality.krml obj/FStar_Set.krml obj/FStar_PredicateExtensionality.krml obj/FStar_WellFounded.krml obj/FStar_Universe.krml obj/Steel_Heap.krml obj/Steel_Memory.krml obj/FStar_MST.krml obj/FStar_NMST.krml obj/Steel_Semantics_Hoare_MST.krml obj/Steel_Semantics_Instantiate.krml obj/FStar_Exn.krml obj/FStar_Monotonic_Witnessed.krml obj/FStar_ErasedLogic.krml obj/FStar_TSet.krml obj/FStar_Monotonic_Heap.krml obj/FStar_Heap.krml obj/FStar_ST.krml obj/FStar_All.krml obj/FStar_List.krml obj/FStar_String.krml obj/FStar_Reflection_V2_TermEq.krml obj/FStar_Tactics_Typeclasses.krml obj/FStar_Tactics_MApply.krml obj/FStar_Tactics_V2_Logic.krml obj/FStar_Tactics_V2.krml obj/FStar_Tactics_CanonCommSwaps.krml obj/FStar_Algebra_CommMonoid_Equiv.krml obj/FStar_Tactics_CanonCommMonoidSimple_Equiv.krml obj/Steel_Effect_Common.krml obj/Steel_Effect.krml obj/Steel_Effect_Atomic.krml obj/Steel_ST_Effect.krml obj/Steel_ST_Effect_AtomicAndGhost.krml obj/Steel_ST_Effect_Atomic.krml obj/Steel_ST_Effect_Ghost.krml obj/Steel_ST_Coercions.krml obj/Steel_PCMReference.krml obj/Steel_PCMFrac.krml obj/Steel_HigherReference.krml obj/Steel_Reference.krml obj/Steel_Loops.krml obj/Steel_ST_Util.krml obj/Steel_ST_Loops.krml obj/Steel_ST_Reference.krml obj/FStar_Map.krml obj/Steel_PCMMap.krml obj/Steel_ST_PCMReference.krml obj/Steel_ST_HigherArray.krml obj/Steel_ST_Array.krml obj/Steel_Array.krml obj/Prelude.krml obj/Config.krml obj/Utils2.krml obj/NullOrVarray.krml obj/Steel_ArrayArith.krml obj/Bitmap5.krml obj/SteelVRefineDep.krml obj/SteelOptUtils.krml obj/SteelStarSeqUtils.krml obj/SlotsAlloc.krml obj/MemoryTrap.krml obj/Quarantine.krml obj/FStar_FiniteSet_Base.krml obj/FStar_FiniteSet_Ambient.krml obj/Steel_ArrayRef.krml obj/ArrayListGen.krml obj/Helpers.krml obj/Guards.krml obj/ArrayList.krml obj/SteelVRefine2.krml obj/SlabsCommon.krml obj/SlotsFree.krml obj/SlabsFree.krml obj/MiscArith.krml obj/SlabsAlloc.krml obj/SizeClass.krml obj/Steel_SpinLock.krml obj/Mman.krml obj/Spec_Trees.krml obj/Spec_BST.krml obj/Impl_Common.krml obj/Steel_TLArray.krml obj/Main.krml obj/Impl_Core.krml obj/Impl_Trees_Types.krml obj/Impl_Trees_M.krml obj/Spec_AVL.krml obj/Spec.krml obj/Impl_BST_M.krml obj/Impl_Trees_Rotate3_M.krml obj/Impl_Trees_Rotate2_M.krml obj/Impl_Trees_Rotate_M.krml obj/Impl_AVL_M.krml obj/Impl_Mono.krml obj/Map_M.krml obj/LargeAlloc.krml obj/ROArray.krml obj/Main_Meta.krml obj/StarMalloc.krml
KaRaMeL invocation: /nix/store/2sp1lmf9zg6snpma319jxhf0hv4hkcpj-karamel-5c7ac22a85fb0b9ce8c278084665022bf7dbb3f7-home/krml -skip-compilation -fparentheses -tmpdir dist -library Steel.ArrayArith -static-header Steel.ArrayArith -no-prefix Steel.ArrayArith -bundle Steel.SpinLock= -bundle FStar.\*,Steel.\* -bundle StarMalloc=Map.\*,Impl.\*,Spec.\*,Main,Main.Meta,LargeAlloc[rename=StarMalloc] -bundle SlabsCommon,SlabsFree,SlabsAlloc[rename=Slabs] -bundle SlotsFree,SlotsAlloc[rename=Slots] -bundle ArrayList,ArrayListGen[rename=ArrayList] -no-prefix Main -no-prefix LargeAlloc -no-prefix Mman -no-prefix MemoryTrap -warn-error +9 -add-include Steel_SpinLock:"steel_types.h" -add-include Steel_SpinLock:"steel_base.h" obj/prims.krml obj/FStar_Pervasives_Native.krml obj/FStar_Pervasives.krml obj/FStar_Mul.krml obj/FStar_Squash.krml obj/FStar_Classical.krml obj/FStar_Preorder.krml obj/FStar_Sealed.krml obj/FStar_Range.krml obj/FStar_Calc.krml obj/FStar_StrongExcludedMiddle.krml obj/FStar_Classical_Sugar.krml obj/FStar_List_Tot_Base.krml obj/FStar_List_Tot_Properties.krml obj/FStar_List_Tot.krml obj/FStar_Seq_Base.krml obj/FStar_Seq_Properties.krml obj/FStar_Seq.krml obj/FStar_Math_Lib.krml obj/FStar_Math_Lemmas.krml obj/FStar_BitVector.krml obj/FStar_UInt.krml obj/FStar_UInt32.krml obj/FStar_Int.krml obj/FStar_Int16.krml obj/Seq2.krml obj/Bitmap1.krml obj/Bitmap2.krml obj/FStar_UInt64.krml obj/Bitmap3.krml obj/Bitmap4.krml obj/FStar_Int64.krml obj/FStar_Int32.krml obj/FStar_Int8.krml obj/FStar_UInt16.krml obj/FStar_UInt8.krml obj/FStar_Int_Cast.krml obj/FStar_Ghost.krml obj/FStar_SizeT.krml obj/SeqUtils.krml obj/FStar_VConfig.krml obj/FStar_Float.krml obj/FStar_Char.krml obj/FStar_Pprint.krml obj/FStar_Issue.krml obj/FStar_TypeChecker_Core.krml obj/FStar_Tactics_Common.krml obj/FStar_Reflection_Types.krml obj/FStar_Tactics_Types.krml obj/FStar_Tactics_Result.krml obj/FStar_Monotonic_Pure.krml obj/FStar_Tactics_Effect.krml obj/FStar_Tactics_Unseal.krml obj/FStar_Sealed_Inhabited.krml obj/FStar_Syntax_Syntax.krml obj/FStar_Reflection_V2_Data.krml obj/FStar_Order.krml obj/FStar_Reflection_V2_Builtins.krml obj/FStar_Reflection_Const.krml obj/FStar_Tactics_V2_Builtins.krml obj/FStar_Tactics_SMT.krml obj/FStar_Tactics_Util.krml obj/FStar_Reflection_V2_Derived.krml obj/FStar_Reflection_V2_Compare.krml obj/FStar_Reflection_V2_Derived_Lemmas.krml obj/FStar_Reflection_V2.krml obj/FStar_Tactics_Visit.krml obj/FStar_Tactics_NamedView.krml obj/FStar_PropositionalExtensionality.krml obj/FStar_Reflection_V1_Data.krml obj/FStar_Reflection_V1_Builtins.krml obj/FStar_Tactics_V1_Builtins.krml obj/FStar_Tactics_Builtins.krml obj/FStar_Tactics_V2_SyntaxCoercions.krml obj/FStar_Tactics_V2_SyntaxHelpers.krml obj/FStar_Reflection_V2_Formula.krml obj/FStar_Tactics_V2_Derived.krml obj/FStar_Tactics_Print.krml obj/FStar_IndefiniteDescription.krml obj/FStar_Reflection_V1_Derived.krml obj/FStar_Reflection_V1_Formula.krml obj/FStar_Reflection_V1_Compare.krml obj/FStar_Reflection_V1_Derived_Lemmas.krml obj/FStar_Reflection_V1.krml obj/FStar_Tactics_V1_SyntaxHelpers.krml obj/FStar_Tactics_V1_Derived.krml obj/FStar_Tactics_V1_Logic.krml obj/FStar_Tactics_V1.krml obj/FStar_Tactics.krml obj/FStar_PtrdiffT.krml obj/FStar_Real.krml obj/Steel_FractionalPermission.krml obj/FStar_Witnessed_Core.krml obj/FStar_MSTTotal.krml obj/FStar_NMSTTotal.krml obj/FStar_PCM.krml obj/Steel_Preorder.krml obj/FStar_FunctionalExtensionality.krml obj/FStar_Set.krml obj/FStar_PredicateExtensionality.krml obj/FStar_WellFounded.krml obj/FStar_Universe.krml obj/Steel_Heap.krml obj/Steel_Memory.krml obj/FStar_MST.krml obj/FStar_NMST.krml obj/Steel_Semantics_Hoare_MST.krml obj/Steel_Semantics_Instantiate.krml obj/FStar_Exn.krml obj/FStar_Monotonic_Witnessed.krml obj/FStar_ErasedLogic.krml obj/FStar_TSet.krml obj/FStar_Monotonic_Heap.krml obj/FStar_Heap.krml obj/FStar_ST.krml obj/FStar_All.krml obj/FStar_List.krml obj/FStar_String.krml obj/FStar_Reflection_V2_TermEq.krml obj/FStar_Tactics_Typeclasses.krml obj/FStar_Tactics_MApply.krml obj/FStar_Tactics_V2_Logic.krml obj/FStar_Tactics_V2.krml obj/FStar_Tactics_CanonCommSwaps.krml obj/FStar_Algebra_CommMonoid_Equiv.krml obj/FStar_Tactics_CanonCommMonoidSimple_Equiv.krml obj/Steel_Effect_Common.krml obj/Steel_Effect.krml obj/Steel_Effect_Atomic.krml obj/Steel_ST_Effect.krml obj/Steel_ST_Effect_AtomicAndGhost.krml obj/Steel_ST_Effect_Atomic.krml obj/Steel_ST_Effect_Ghost.krml obj/Steel_ST_Coercions.krml obj/Steel_PCMReference.krml obj/Steel_PCMFrac.krml obj/Steel_HigherReference.krml obj/Steel_Reference.krml obj/Steel_Loops.krml obj/Steel_ST_Util.krml obj/Steel_ST_Loops.krml obj/Steel_ST_Reference.krml obj/FStar_Map.krml obj/Steel_PCMMap.krml obj/Steel_ST_PCMReference.krml obj/Steel_ST_HigherArray.krml obj/Steel_ST_Array.krml obj/Steel_Array.krml obj/Prelude.krml obj/Config.krml obj/Utils2.krml obj/NullOrVarray.krml obj/Steel_ArrayArith.krml obj/Bitmap5.krml obj/SteelVRefineDep.krml obj/SteelOptUtils.krml obj/SteelStarSeqUtils.krml obj/SlotsAlloc.krml obj/Helpers.krml obj/MemoryTrap.krml obj/Quarantine.krml obj/FStar_FiniteSet_Base.krml obj/FStar_FiniteSet_Ambient.krml obj/Steel_ArrayRef.krml obj/SetUtils.krml obj/ArrayListGen.krml obj/ArrayList.krml obj/Guards.krml obj/SteelVRefine2.krml obj/SlabsCommon.krml obj/SlotsFree.krml obj/SlabsFree.krml obj/MiscArith.krml obj/SlabsAlloc.krml obj/SizeClass.krml obj/Steel_SpinLock.krml obj/Mman.krml obj/Spec_Trees.krml obj/Spec_BST.krml obj/Impl_Common.krml obj/Steel_TLArray.krml obj/Main.krml obj/Impl_Core.krml obj/Impl_Trees_Types.krml obj/Impl_Trees_M.krml obj/Spec_AVL.krml obj/Spec.krml obj/Impl_BST_M.krml obj/Impl_Trees_Rotate3_M.krml obj/Impl_Trees_Rotate2_M.krml obj/Impl_Trees_Rotate_M.krml obj/Impl_AVL_M.krml obj/Impl_Mono.krml obj/Map_M.krml obj/LargeAlloc.krml obj/ROArray.krml obj/Main_Meta.krml obj/StarMalloc.krml
F* version: <unknown>
KaRaMeL version: <unknown>
*/
Expand Down Expand Up @@ -88,6 +88,8 @@ ArrayList_extend_insert(
size_t hd3,
size_t hd4,
size_t hd5,
size_t tl5,
size_t sz5,
size_t k,
uint32_t v1
)
Expand All @@ -97,6 +99,8 @@ ArrayList_extend_insert(
KRML_MAYBE_UNUSED_VAR(hd3);
KRML_MAYBE_UNUSED_VAR(hd4);
KRML_MAYBE_UNUSED_VAR(hd5);
KRML_MAYBE_UNUSED_VAR(tl5);
KRML_MAYBE_UNUSED_VAR(sz5);
extend_insert__uint32_t(n2, r, k, v1);
}

Loading

0 comments on commit 04bf0ad

Please sign in to comment.