From 90635615e36dbc7da013d3d1bad7e4cdb80c1573 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 8 Jan 2025 14:22:49 -0800 Subject: [PATCH 1/2] Improved compilation scheme for enums. Now that we allow choosing values for enum constants, there are two compilation schemes for enums (i.e., data types where no constructor takes arguments). - C11 enums, i.e., `typedef enum { A = 0xff, ... } t;`. These are mandated to have type `int` in C11; C23 allows choosing the width, but we don't yet assume C23. We assume `sizeof int == 4` and error out if any of the user-chosen constants exceed the range of `int`. - Macros. We cannot represent arithmetic on enum constants, so there are no issues about integer promotions, or a constant being sign-extended for the wrong reasons. We just print out integer literals, and try the first type that fits all possible values for the enum type, with a preference for unsigned types. This fixes AeneasVerif/eurydice#123 --- krmllib/hints/C.Endianness.fst.hints | 44 +++--- krmllib/hints/C.Failure.fst.hints | 4 +- krmllib/hints/C.Loops.fst.hints | 78 +++++------ krmllib/hints/C.String.fst.hints | 18 +-- krmllib/hints/C.String.fsti.hints | 10 +- krmllib/hints/C.fst.hints | 2 +- krmllib/hints/FStar.Krml.Endianness.fst.hints | 130 +++++++++--------- krmllib/hints/LowStar.Lib.AssocList.fst.hints | 28 ++-- .../hints/LowStar.Lib.LinkedList.fst.hints | 58 ++++---- .../hints/LowStar.Lib.LinkedList2.fst.hints | 42 +++--- krmllib/hints/Spec.Loops.fst.hints | 34 ++--- krmllib/hints/TestLib.fsti.hints | 4 +- krmllib/hints/WasmSupport.fst.hints | 6 +- lib/Ast.ml | 3 +- lib/AstToCFlat.ml | 6 +- lib/C11.ml | 2 +- lib/CStar.ml | 2 +- lib/CStarToC11.ml | 44 ++++-- lib/DataTypes.ml | 2 +- lib/PrintAst.ml | 4 +- lib/PrintC.ml | 13 +- 21 files changed, 283 insertions(+), 251 deletions(-) diff --git a/krmllib/hints/C.Endianness.fst.hints b/krmllib/hints/C.Endianness.fst.hints index 0f0dcab4..043c3e71 100644 --- a/krmllib/hints/C.Endianness.fst.hints +++ b/krmllib/hints/C.Endianness.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "ee34298a0075e2049a5c23768def7709" + "3270c30260564865ead51978821eb010" ], [ "C.Endianness.load16_le", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "059492a2f31f53307a760a6b60fd7e21" + "cf4f5ae5bc25dc9a54e5350b2310fc98" ], [ "C.Endianness.store16_be", @@ -26,7 +26,7 @@ 1, [ "@query" ], 0, - "2747d49fced7dd76bbecce24721d8a54" + "d2fa85f1e0a79ebabf517038da14c332" ], [ "C.Endianness.load16_be", @@ -35,7 +35,7 @@ 1, [ "@query" ], 0, - "63b268ccf8692eae298896b422e1cd58" + "29a3819ff037e7a9d504d9050eea2386" ], [ "C.Endianness.store32_le", @@ -44,7 +44,7 @@ 1, [ "@query" ], 0, - "5b6357760dceba9b639a4478b9772289" + "a5ad216a13ebc18d6acb2fcb301ace60" ], [ "C.Endianness.load32_le", @@ -53,7 +53,7 @@ 1, [ "@query" ], 0, - "12089361bf2fd7fc2b595d307909b57e" + "06c1b8f82dc2cd6a1252cfe6c4113107" ], [ "C.Endianness.store32_be", @@ -62,7 +62,7 @@ 1, [ "@query" ], 0, - "babec18969e5f4e39144d99878fe998d" + "9a3a779244ec22a6b10235427ddcd3f3" ], [ "C.Endianness.load32_be", @@ -71,7 +71,7 @@ 1, [ "@query" ], 0, - "2cf359a8215ceede0fab7e7a4ba084ea" + "585291395ad3cb3a4531df3d12a2b1b0" ], [ "C.Endianness.store64_le", @@ -80,7 +80,7 @@ 1, [ "@query" ], 0, - "d61ae04f7484f07623814a211fdc11fa" + "aa21fe469eb776e7b42ff11128c20613" ], [ "C.Endianness.load64_le", @@ -89,7 +89,7 @@ 1, [ "@query" ], 0, - "dc7f0b53e54389e81dfe18ee6b3d5285" + "a4d8c309467614857c147f7d66a88508" ], [ "C.Endianness.load64_be", @@ -98,7 +98,7 @@ 1, [ "@query" ], 0, - "4ebbb7d88d86ff1bc9fa97707f889d14" + "630d96a2778c7c68b0a7693d3fe8af0f" ], [ "C.Endianness.store64_be", @@ -107,7 +107,7 @@ 1, [ "@query" ], 0, - "ca313aa1d720a858b5db8ec04ff71f43" + "ebf52bfaec92d336f1243380a13f4659" ], [ "C.Endianness.load128_le", @@ -119,7 +119,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "82b8ede11dfe32b7200a037a5fde3528" + "b44ba2ac191c415bcd2f989bb670ed9f" ], [ "C.Endianness.store128_le", @@ -131,7 +131,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "f360fbae26157e6238cbd56d0b0cb5b8" + "c8c9b32dac57e06038fd453b17a3390c" ], [ "C.Endianness.load128_be", @@ -143,7 +143,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "f77ae3ba525059b52cda52bbdbd83251" + "fbdf443ceee4d4759a29c9f00ae42fa5" ], [ "C.Endianness.store128_be", @@ -155,7 +155,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "a40c46bf89e02f69b9ce5c95cd6011b8" + "48403bf4414798b7812d50589502fcf6" ], [ "C.Endianness.index_32_be", @@ -212,7 +212,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "81678ebf003387795e32689026c08af8" + "a2b21bd114b9abe4151d74cdedc440af" ], [ "C.Endianness.index_32_le", @@ -274,7 +274,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "0a66374405d193035056f995612b1939" + "a9400aaddbe2b861461e281bb8a111a3" ], [ "C.Endianness.index_64_be", @@ -331,7 +331,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "d3f15cf5725e7f32e9c739bfbad8772e" + "5cfcd7fdb363ade9a4672dd9d0c2e72b" ], [ "C.Endianness.index_64_le", @@ -388,7 +388,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "4d5af36f915562dc9f2707bb968a8b13" + "59c219d98b8e571bd785cf711a2df142" ], [ "C.Endianness.interval_4_disjoint", @@ -405,7 +405,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "b6a6b38cf8aa22f925d4f135f13eec35" + "094c7441e541cdfe53c5fc00ac59e3ed" ], [ "C.Endianness.upd_32_be", @@ -483,7 +483,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "2300fa79184ef376a92ac6bdb293de70" + "ab22c315bf713df45c746bee61afd056" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Failure.fst.hints b/krmllib/hints/C.Failure.fst.hints index 0a26683f..5f1878b8 100644 --- a/krmllib/hints/C.Failure.fst.hints +++ b/krmllib/hints/C.Failure.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "6b6c3f900ac6388b602310917e66c467" + "08d81f58fba97609ae70de28e0d0ed43" ], [ "C.Failure.failwith", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "28e8d8148726813436fde85bb1752f0a" + "dd087548f9c6d1b4b6925043c38bd2d5" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Loops.fst.hints b/krmllib/hints/C.Loops.fst.hints index 595f3791..468b9651 100644 --- a/krmllib/hints/C.Loops.fst.hints +++ b/krmllib/hints/C.Loops.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.UInt32.v" ], 0, - "e8561266fbe1048750331fef51e8d661" + "370e4d7f8d2908149b2da94f298f0fc7" ], [ "C.Loops.for", @@ -60,7 +60,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "54a20014fcc3fbdbec7d43107d306764" + "78d77c7fa4011a24d96433d19b9165eb" ], [ "C.Loops.for", @@ -80,7 +80,7 @@ "typing_FStar.UInt32.v" ], 0, - "5afb58b4071316a1473ff2b040c2576f" + "445039afb7cbf9010a9b2d085997d039" ], [ "C.Loops.for64", @@ -101,7 +101,7 @@ "typing_FStar.UInt64.v" ], 0, - "fba3a0e885622afe8c918fcde11a7749" + "7b520fad84e2e3cf77fb33b3433b19d0" ], [ "C.Loops.for64", @@ -141,7 +141,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt64.v" ], 0, - "8da1edeba0451a7150c5791734ea06e3" + "3d3ad5a0ad04ffa7a9c9b2f93c126ba9" ], [ "C.Loops.for64", @@ -161,7 +161,7 @@ "typing_FStar.UInt64.v" ], 0, - "0c6b9403bd8e3c71af4c686a418feb6c" + "927d07423cdf25e54467decb51ec4e46" ], [ "C.Loops.reverse_for", @@ -183,7 +183,7 @@ "typing_FStar.UInt32.v" ], 0, - "b4f91316af9cc7f8c472735066df2d64" + "f2322c34f529a75ed315228c5131ae7e" ], [ "C.Loops.reverse_for", @@ -224,7 +224,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "03e5179d6e656c8bd76713ee3a543189" + "07f5bb62972de820ae38799cf72ebcff" ], [ "C.Loops.reverse_for", @@ -246,7 +246,7 @@ "typing_FStar.UInt32.v" ], 0, - "598f068fdacc99d0d54a059cb4c1d092" + "e9a48c5157fce5b1b5004156edd62113" ], [ "C.Loops.interruptible_for", @@ -266,7 +266,7 @@ "typing_FStar.UInt32.v" ], 0, - "63d29d63346c8ac01d53e3cc10411377" + "18ce1b56522c5abbef61129fb93f8321" ], [ "C.Loops.interruptible_for", @@ -310,7 +310,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "3e438d338f5cf1d70217eeae4cd37b1c" + "71fa1da97a34580d9a9721e0cb751ddb" ], [ "C.Loops.interruptible_for", @@ -330,7 +330,7 @@ "typing_FStar.UInt32.v" ], 0, - "c169d4bb624bc046ff9c92797671b2e2" + "e3b79924b112ac8d48a4659107eeec68" ], [ "C.Loops.do_while", @@ -355,7 +355,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "70623d72e2208de0e8c847e971674f39" + "383c79db2dfb0d647b66771ffa1b46fb" ], [ "C.Loops.while", @@ -369,7 +369,7 @@ "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb" ], 0, - "c1ead9cd7d4e755832485c55efcc8bf4" + "a8be069f76cab54808f8d140452dc314" ], [ "C.Loops.interruptible_reverse_for", @@ -391,7 +391,7 @@ "typing_FStar.UInt32.v" ], 0, - "9dc56c7594b0c7e8e69623fe3599ceec" + "1b518770d956425c862c30ec60ab35ca" ], [ "C.Loops.interruptible_reverse_for", @@ -436,7 +436,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "15a38ac29b0289c48412520598b20310" + "64c101119639e3ca67a6bcec73375833" ], [ "C.Loops.interruptible_reverse_for", @@ -458,7 +458,7 @@ "typing_FStar.UInt32.v" ], 0, - "77f792bd136fc29cfbe43eee44d46be0" + "4c22047b3d308bde06b038cfff141523" ], [ "C.Loops.map", @@ -467,7 +467,7 @@ 1, [ "@query" ], 0, - "a2fa607283b571f4251f0a612c5a2929" + "fd9fa61ec78ccdc71a3b255fa0a65843" ], [ "C.Loops.map", @@ -516,7 +516,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "986ebeeb3ee07e7a8a96aaad8708653e" + "71e1adac519203c91205165f7f307f42" ], [ "C.Loops.map", @@ -525,7 +525,7 @@ 1, [ "@query" ], 0, - "23408047f351a86f84c9ba7e293e3a05" + "6ce24e9af2e22628b69375430e0665a6" ], [ "C.Loops.map2", @@ -540,7 +540,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "79f45d97edeb8c1ef31230edc16581d0" + "b00d6e6f925269d96724a19c489c2a3b" ], [ "C.Loops.map2", @@ -589,7 +589,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "0d8cbb0ff1040c8c8c04f5e94ddbb4c2" + "adbec8bb73343fe77f4977be075a5c3f" ], [ "C.Loops.map2", @@ -598,7 +598,7 @@ 1, [ "@query" ], 0, - "cacb0b69ea8274cd366dac5c2a4a847b" + "5613ce73658a1a90bb01dce89c3cd036" ], [ "C.Loops.in_place_map", @@ -607,7 +607,7 @@ 1, [ "@query" ], 0, - "9ac2d23f2410df6e665d4a18e4b652a3" + "4b2e1f86ac6213277d471ee6f2425cbf" ], [ "C.Loops.in_place_map", @@ -652,7 +652,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "d3557778899a306b0c4d7f05df2229f3" + "6ecbaa516d14fe89bdde4671e7c1dda9" ], [ "C.Loops.in_place_map", @@ -661,7 +661,7 @@ 1, [ "@query" ], 0, - "1a7f7aa197db1eacd5f93cad5ed58193" + "397f90c7dd222b03469ba4934fd8bad4" ], [ "C.Loops.in_place_map2", @@ -676,7 +676,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "9eee135b034b0ddd6fdca19607ae18ab" + "d75101939c4c454bad59a5d97bd4e008" ], [ "C.Loops.in_place_map2", @@ -723,7 +723,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "864aa03e99c3bd20257ab2438fb71f15" + "5707a2dc030c117a5e5b56f2b2fd5a99" ], [ "C.Loops.in_place_map2", @@ -732,7 +732,7 @@ 1, [ "@query" ], 0, - "52796be010e5f200ae66d84549219204" + "a855680bd3738d8691ee3ef403e6a3c0" ], [ "C.Loops.repeat", @@ -755,7 +755,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "3e927a5f0bc1666725686276abd28b19" + "7ec2561339c9f8c0bf698f1f9e5c768b" ], [ "C.Loops.repeat", @@ -788,7 +788,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "cbbb2d4dadc1a65bfd5fa0f3e2a51579" + "0f6b5676f9c2875c2029c4ef2000ab91" ], [ "C.Loops.repeat", @@ -806,7 +806,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "0406c679fc79557761ff9018602dca0a" + "b102d35536683224154c5fac86501755" ], [ "C.Loops.repeat_range_body_impl", @@ -825,7 +825,7 @@ "typing_FStar.UInt32.v" ], 0, - "6f953dc630c6f8025c2d97c572bdd5ea" + "bb3841004ef05cfae5644d4e35e06cd2" ], [ "C.Loops.repeat_range_body_impl", @@ -839,7 +839,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "8be353174a8de28928078cd1f915f630" + "b30864483c112752b8c94ea5aa2e4132" ], [ "C.Loops.repeat_range", @@ -858,7 +858,7 @@ "typing_FStar.UInt32.v" ], 0, - "c494c9a82ba6b4abb0fff46c4ac2c690" + "7f357046d2c3028611c8aed717ce66d3" ], [ "C.Loops.repeat_range", @@ -883,7 +883,7 @@ "typing_FStar.UInt32.v" ], 0, - "54dc862acea8eb47aa59a055629496d0" + "6f57fa6be729de297497b5a94dd56572" ], [ "C.Loops.repeat_range", @@ -897,7 +897,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "3657db8f0677890ff61293ff3fb1dc1b" + "a632cc0e5feba94d31e3be4402809924" ], [ "C.Loops.total_while_gen", @@ -910,7 +910,7 @@ "binder_x_245a4248f315846e90b81e2d076a282b_6", "bool_inversion" ], 0, - "d05bb7ade2bb9385a7a7d7f6b02440a6" + "3fa5d7a54253850e6fee932fedec36f7" ], [ "C.Loops.total_while", @@ -929,7 +929,7 @@ "well-founded-ordering-on-nat" ], 0, - "a4bdffff8983525d73ee6c342fba8cc4" + "599a24c6030b6f0b2a039722bff38936" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fst.hints b/krmllib/hints/C.String.fst.hints index 8e947093..0b6ff93b 100644 --- a/krmllib/hints/C.String.fst.hints +++ b/krmllib/hints/C.String.fst.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "64e3354798a244f79f4d7ed5ecd83f6a" + "55c7ef67c0b3e150fd366a90185ffcb7" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "48349ba40bf25deed03f8e1d4225a028" + "96f67f33fb53eddddb82da94d0fafafd" ], [ "C.String.t", @@ -35,7 +35,7 @@ "lemma_FStar.Seq.Base.hasEq_lemma" ], 0, - "18184b474bfdd7d26320e397347eaf19" + "c88d42ae53ebe87c6346f593ac6fcdf4" ], [ "C.String.length", @@ -50,7 +50,7 @@ "refinement_interpretation_Tm_refine_ed6e8a85e123e1e628ba0dad885f3031" ], 0, - "9499b9fb7e55cd8dee288ea18b8c2b69" + "bda33aff6dd88cc901a87c7be511ebfb" ], [ "C.String.get", @@ -66,7 +66,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "f857c485db002cdf65944f548a6769a1" + "96933c3efb18d7ad78a6d8001b01620e" ], [ "C.String.get", @@ -85,7 +85,7 @@ "typing_FStar.UInt32.v" ], 0, - "5acc1d39389927b71928ad7bda8d2d43" + "194bf25c3cf63e0cc6d6334ff61f9f6f" ], [ "C.String.nonzero_is_lt", @@ -98,7 +98,7 @@ "fuel_guarded_inversion_C.String.t" ], 0, - "e0d8fe9c6ce0ffce4457ef58dd101bb8" + "285d07d9baf4044d0547598c500b3ea7" ], [ "C.String.nonzero_is_lt", @@ -119,7 +119,7 @@ "typing_FStar.UInt32.v" ], 0, - "f9fe79f2a249f81b518c6c6458e489d0" + "90f1da2436e1b8b025f01c692e5538bd" ], [ "C.String.memcpy", @@ -133,7 +133,7 @@ "typing_FStar.UInt8.t" ], 0, - "30b5d41500a118562a290de3a9ad5075" + "cad4b92446b988f37ff5bc8db5a99e17" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fsti.hints b/krmllib/hints/C.String.fsti.hints index ea940da5..a02b6d3e 100644 --- a/krmllib/hints/C.String.fsti.hints +++ b/krmllib/hints/C.String.fsti.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "f6f6826a2aadc2fc264dc903f6c54396" + "73c2f65c8c1e750f8730150ffce38cbb" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "48349ba40bf25deed03f8e1d4225a028" + "ffc703503f3fdc9a3226bb383e4ae9bb" ], [ "C.String.get", @@ -39,7 +39,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "15df9cb4283bbdadaf567740c065d1d0" + "cfd75e795ca5cdb85fef9fd47d47071c" ], [ "C.String.nonzero_is_lt", @@ -52,7 +52,7 @@ "typing_C.String.length" ], 0, - "8284e4302eac3346933d4cfe323be989" + "e5ed4cc60955f005bcb2c70fd4e809cf" ], [ "C.String.memcpy", @@ -66,7 +66,7 @@ "typing_FStar.UInt8.t" ], 0, - "0457f5f95f9adc9a049ec8b972177613" + "8daac024e2a02c802f700da6bf5c834f" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.fst.hints b/krmllib/hints/C.fst.hints index ff8f93f3..c7742e5d 100644 --- a/krmllib/hints/C.fst.hints +++ b/krmllib/hints/C.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query", "assumption_C.HasEq_char" ], 0, - "c0c9374a78617f794d4bb9657f920cdb" + "843f503ca3a9719b65d83d79dc39e0fc" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/FStar.Krml.Endianness.fst.hints b/krmllib/hints/FStar.Krml.Endianness.fst.hints index c8b63f52..b00e439e 100644 --- a/krmllib/hints/FStar.Krml.Endianness.fst.hints +++ b/krmllib/hints/FStar.Krml.Endianness.fst.hints @@ -32,7 +32,7 @@ "well-founded-ordering-on-nat" ], 0, - "5df4ba1cee764292c0d5477b678d0047" + "239cce79aebc8fc0453760651800cd0f" ], [ "FStar.Krml.Endianness.be_to_n", @@ -65,7 +65,7 @@ "well-founded-ordering-on-nat" ], 0, - "26dac893779b32995b0658a9236732e5" + "c3547249bc5ff0da1e756bd337cac623" ], [ "FStar.Krml.Endianness.lemma_euclidean_division", @@ -77,7 +77,7 @@ "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, - "86a085f374d331feedc06da469431d39" + "0154ec24e007481ee977b097bf41b4db" ], [ "FStar.Krml.Endianness.lemma_factorise", @@ -90,7 +90,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "f639e801cd4e13c8100b5bc49e9ca10a" + "5b42abfd2cd333c31f51f8ebabab9002" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -107,7 +107,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "fb290993a3e1f97b03ac22f1082c6f4a" + "eb9bf077c04b2251d5f88e7689b5a762" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -149,7 +149,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "f7b55f35ffc48ebac5cb638b2fa2da23" + "f4e28777a088536e74dbd2539a1180c8" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -167,7 +167,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "559054cb4780740312bd62e86f734025" + "7a6813625045c882f2cbe9c8c1353f4f" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -184,7 +184,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "7ee5429b5937b3a0aceb0756e1b62e3c" + "81a07fc3c925adc49b68d95760e24ef1" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -223,7 +223,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "41369fce5c4c8471dfb9637cbb8af161" + "99c481f1e8f1b9a2acb360499a427ecc" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -241,7 +241,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "1954adc433bbb5928561875c970d6e58" + "3eb5524c7aef27fb0700da6c74db9832" ], [ "FStar.Krml.Endianness.n_to_le", @@ -260,7 +260,7 @@ "typing_FStar.UInt32.v" ], 0, - "92ba7267241642cf67abf56d9468916a" + "0c50bc2e92677b6b210e9b518f8e4ad4" ], [ "FStar.Krml.Endianness.n_to_le", @@ -322,7 +322,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "3abc1bc25f060f4539a066bd4b630043" + "6dcf5db46b671ab3ace985055bf41dc8" ], [ "FStar.Krml.Endianness.n_to_le", @@ -341,7 +341,7 @@ "typing_FStar.UInt32.v" ], 0, - "1ec80ce44654bf0e2fe75c4d4d506fe0" + "5862acff99bf5de93c0e6268ad24c639" ], [ "FStar.Krml.Endianness.n_to_be", @@ -360,7 +360,7 @@ "typing_FStar.UInt32.v" ], 0, - "9983c08bd2bec69ede03c5f9355eb47f" + "3948025eccf64e1365ad417d9f42103c" ], [ "FStar.Krml.Endianness.n_to_be", @@ -423,7 +423,7 @@ "well-founded-ordering-on-nat" ], 0, - "2f3cc9e39c4758e0d0bb429bbd4204c3" + "98cb1814666fd2c4a3a60848ae718906" ], [ "FStar.Krml.Endianness.n_to_be", @@ -442,7 +442,7 @@ "typing_FStar.UInt32.v" ], 0, - "404db1d59ec1bb422181f46793de6af6" + "116d723c1d6ea5e461ab06de01f7b9f1" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -464,7 +464,7 @@ "typing_FStar.Krml.Endianness.n_to_le", "typing_FStar.UInt32.v" ], 0, - "2b27b180b8e2406621999d7a2b59bbf0" + "283e5f3f258839537d3386f7c6a6c784" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -483,7 +483,7 @@ "typing_FStar.UInt32.v" ], 0, - "a3c6ac9970113a90f3cb7da604591907" + "9b9992be1faefac8b9b927334ba5e3be" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -505,7 +505,7 @@ "typing_FStar.Krml.Endianness.n_to_be", "typing_FStar.UInt32.v" ], 0, - "c02694739e3a34e770db69b4899dd482" + "2e4201f863bf432ac101791fc671e921" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -524,7 +524,7 @@ "typing_FStar.UInt32.v" ], 0, - "a3c6ac9970113a90f3cb7da604591907" + "533cb85497df951a750c10be696d1b7b" ], [ "FStar.Krml.Endianness.be_to_n_inj", @@ -580,7 +580,7 @@ "well-founded-ordering-on-nat" ], 0, - "def5a94071807c95c4e17b3da9c2c463" + "82b52988ba97aab024431c56ad4abd48" ], [ "FStar.Krml.Endianness.le_to_n_inj", @@ -643,7 +643,7 @@ "typing_FStar.UInt8.v", "well-founded-ordering-on-nat" ], 0, - "94c02ef7097d770e5ab513306c812077" + "14e3f1304073087d7371961acc3125ed" ], [ "FStar.Krml.Endianness.n_to_be_be_to_n", @@ -662,7 +662,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "a38685dd7ff14481a266c177da1b9cf0" + "0498e161132c193136f2820e52dd6fea" ], [ "FStar.Krml.Endianness.n_to_le_le_to_n", @@ -681,7 +681,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "0c19eb4a35f02502005aee62d077b4a0" + "f649deb76decac503933a1c2cd8dd545" ], [ "FStar.Krml.Endianness.uint32_of_le", @@ -701,7 +701,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "6f1cfd4a4e3e5afce324f420b1855bf0" + "537005682ddc159087872bca01f6a801" ], [ "FStar.Krml.Endianness.le_of_uint32", @@ -718,7 +718,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "2b3dc047b554621a231c5ba77da2d06e" + "d97c490db2816a22afe3f14157b8a060" ], [ "FStar.Krml.Endianness.uint32_of_be", @@ -738,7 +738,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "5fc5b8b46340cd9defcc2c7dbf6ca1ab" + "e93868388719f1993fa3ef8a1e832cf6" ], [ "FStar.Krml.Endianness.be_of_uint32", @@ -755,7 +755,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "17585cedbd4a8922c3e6aba2b57521d1" + "ffbacf270d870c7d4acb157a47c5fb81" ], [ "FStar.Krml.Endianness.uint64_of_le", @@ -775,7 +775,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "460147c32683ec521316be94433226e4" + "414309d73a32d64a955a2149818fb95c" ], [ "FStar.Krml.Endianness.le_of_uint64", @@ -792,7 +792,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "6a6f2256e2e7f9d8c65461935a1e0dd5" + "bf74fed2ac3fa8aeb430958c7b014b80" ], [ "FStar.Krml.Endianness.uint64_of_be", @@ -812,7 +812,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "c959ff9b5a921cb9d511f598d906086b" + "c798843fe1d334ba03f8836c5c076eca" ], [ "FStar.Krml.Endianness.be_of_uint64", @@ -829,7 +829,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "3e364be74e7edb43a30fccb8f01a4a50" + "446534ab48f7167464ab0b0c270d50e0" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -869,7 +869,7 @@ "well-founded-ordering-on-nat" ], 0, - "d27f9c2527812d9fcc0c19118edb887e" + "92068a0ca07879cb12f1504f01c92660" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -883,7 +883,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "1d535edd12dd4984b17de47ff1347ea6" + "2f0be11ab9da53eb2f309b16244bbad7" ], [ "FStar.Krml.Endianness.le_of_seq_uint32", @@ -919,7 +919,7 @@ "well-founded-ordering-on-nat" ], 0, - "adf2ecb918b1d767a3c5a96d6ab49f57" + "a40a75f2a68ad92b82f78a891beb6527" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -959,7 +959,7 @@ "well-founded-ordering-on-nat" ], 0, - "12f1721d740d7aa53cf4846d063afea5" + "d1427c458400cfc8ca542c16ec1c9de4" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -973,7 +973,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "d766f0404b2a013cfb35afa0940f71e8" + "468210dfdc252caf0e64b8fb355b1b5d" ], [ "FStar.Krml.Endianness.be_of_seq_uint32", @@ -1009,7 +1009,7 @@ "well-founded-ordering-on-nat" ], 0, - "552519464790fb1ee2243dc60d194971" + "9aef17ea1d2a421ea5f8faa8e1a321ec" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1049,7 +1049,7 @@ "well-founded-ordering-on-nat" ], 0, - "a52be2b9ba8abfab78116d3a1d7987ca" + "3ae5d993a2798850ab457e9af5d82166" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1063,7 +1063,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "6db92134070428cab101d47c3cd9cfcc" + "52f0e6d493972c7da5a4666b75ad7e3c" ], [ "FStar.Krml.Endianness.le_of_seq_uint64", @@ -1099,7 +1099,7 @@ "well-founded-ordering-on-nat" ], 0, - "2728794ce785d00c03df3bbc1136c074" + "a2f08a496178d2eff74390755ed1c5b5" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1139,7 +1139,7 @@ "well-founded-ordering-on-nat" ], 0, - "dc8985e384823875ae7c9f5432f2c82e" + "8580fd90a8c5dbfb805f9d942d20ac50" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1153,7 +1153,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "3d83203064e2757a8981dce7e4e855bf" + "f77a9ad10b3628a383b314c382f1912a" ], [ "FStar.Krml.Endianness.be_of_seq_uint64", @@ -1189,7 +1189,7 @@ "well-founded-ordering-on-nat" ], 0, - "f926a641ec8cb82eb84c1504438b8c18" + "744803708210b33edddb4c14ee0b4b2a" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1257,7 +1257,7 @@ "well-founded-ordering-on-nat" ], 0, - "43791cee2f081327e7250c7a51d4dcc8" + "c4ac15d0244aa1810b3984bdcb6d8dad" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1283,7 +1283,7 @@ "typing_FStar.UInt8.t" ], 0, - "3acc29eddd8e960bcdd19db68de5a1de" + "6c06a7da702d179092016be7ede94268" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1348,7 +1348,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "eebf0f57ee4b482fd9c42129979ed09d" + "bdf6f2851bb345420df997d27d483bb0" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1374,7 +1374,7 @@ "typing_FStar.UInt8.t" ], 0, - "ef1acd7e64ee456d3073220c587061c7" + "d689fcdbe7afc6afc4d956885f3aad9c" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1436,7 +1436,7 @@ "well-founded-ordering-on-nat" ], 0, - "d4e4a0c71a8608109a1d33c7fd93847c" + "dc7f9d0a2add8d478d11d20f50c25580" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1462,7 +1462,7 @@ "typing_FStar.UInt8.t" ], 0, - "34dbf734070f6a2931651f10e9d6086f" + "3ffa011ecbc48e2c2ca8c6f9dba017a9" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1526,7 +1526,7 @@ "well-founded-ordering-on-nat" ], 0, - "8aecc2068e9fc183a63c9243c3bdde02" + "6da2a919e0d70831d117868964d5e3fa" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1552,7 +1552,7 @@ "typing_FStar.UInt8.t" ], 0, - "edd1f91664886423dccaf827adf04523" + "c030a9347b26cbe4b99833dd89a61ca6" ], [ "FStar.Krml.Endianness.tail_cons", @@ -1584,7 +1584,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.tail" ], 0, - "1d6e8d17114f844c1041c642b7c8f2b7" + "2117d1e307a852b0c07bbeef6513d5b0" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_append", @@ -1646,7 +1646,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "c2f6415885e946fdb29a1cc0aa482615" + "6baaa3db41fee18705c882db19bf2528" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_base", @@ -1702,7 +1702,7 @@ "typing_FStar.UInt8.t" ], 0, - "d44263154e8832adccc758cca425cfba" + "4cffea18741411b60dadb34fd08fe119" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_append", @@ -1764,7 +1764,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "022deb7983030ca7f03e86964b8f511d" + "e99fe76c0b56f44854c9de92a17d7a35" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_base", @@ -1820,7 +1820,7 @@ "typing_FStar.UInt8.t" ], 0, - "4193df2587f0eb235a103e5226273df4" + "5e503aaa0e33d2807a7180c7f3e3afe6" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_append", @@ -1882,7 +1882,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "63aa08b6bde3a8d97c9da3e6744f32b7" + "471bb5691c8d59e14f5fd89ba14fcac9" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_base", @@ -1939,7 +1939,7 @@ "typing_FStar.UInt8.t" ], 0, - "b80724b1ffb0739ec6468ca784ef1586" + "3a60d77922339a126197f75a9cad7756" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -2015,7 +2015,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "87d0df8fefd0f8bbc6a09d83c14f215d" + "be0d3da0f3b39f6bc5f0daa8352cc1a3" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -2027,7 +2027,7 @@ "refinement_interpretation_Tm_refine_a84773c2eb377e624aba800b71ec3ba0" ], 0, - "cc8c2f06bf1c886be7d3f15d592f4ed6" + "b99b980b241433ad5cdbfe904516f87a" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2100,7 +2100,7 @@ "well-founded-ordering-on-nat" ], 0, - "8392edaf8b7b128cf8817b7b2a4f676b" + "ef2e7e7192301b7c4bd18597292cbb75" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2112,7 +2112,7 @@ "refinement_interpretation_Tm_refine_4239cb7a019da00e7afc3bc55aa05dd7" ], 0, - "de860d9ec4ddb55d2ed6a70976c7ec0f" + "7507a4f8252b99e9b9019dc3fa078ea9" ], [ "FStar.Krml.Endianness.slice_seq_uint32_of_be", @@ -2162,7 +2162,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt8.t" ], 0, - "5fb745470aafa3dd84ef74a187e77da7" + "51b6b06d25bfde6e6458e805328ce952" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_slice", @@ -2214,7 +2214,7 @@ "typing_FStar.UInt8.t" ], 0, - "5dc8d0d82be8f6cdaab56b5f847b176a" + "219f07f5f9d10f08b9b08a18b8e5714d" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.AssocList.fst.hints b/krmllib/hints/LowStar.Lib.AssocList.fst.hints index ec724013..bcb9e31b 100644 --- a/krmllib/hints/LowStar.Lib.AssocList.fst.hints +++ b/krmllib/hints/LowStar.Lib.AssocList.fst.hints @@ -8,7 +8,7 @@ 0, [ "@query", "equation_LowStar.Lib.AssocList.invariant" ], 0, - "0e9a8ef5b12c274b9c2568a8b61030e9" + "9872a656aa406526da7db52973a31c56" ], [ "LowStar.Lib.AssocList.frame", @@ -74,7 +74,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "735d711fb1c71dd39010b253458fe8c8" + "e0a77629840b30c060f2f06536587064" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -87,7 +87,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "5ad006b564f9651d7246a327bbc7780b" + "9aedf92d6d64bf6cde1aad770583874a" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -103,7 +103,7 @@ "fuel_guarded_inversion_LowStar.Lib.LinkedList2.t" ], 0, - "d5266747289e474c7485a484eda98727" + "1975ce9e9d80c4054bde89318451f7b4" ], [ "LowStar.Lib.AssocList.create_in", @@ -137,7 +137,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "0c86b5365bee21bbaa25eccada221d37" + "58c828c6a9c13aa7ffd140b9749dd502" ], [ "LowStar.Lib.AssocList.find_", @@ -146,7 +146,7 @@ 0, [ "@query" ], 0, - "09ad5facd13c96da33214afaef1113ed" + "227b0be41b55232147528b898e65ec66" ], [ "LowStar.Lib.AssocList.find_", @@ -226,7 +226,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "06f681b80be32f92506d530117a649fb" + "649a547edc5339c1790c87944935443b" ], [ "LowStar.Lib.AssocList.find", @@ -244,7 +244,7 @@ "refinement_interpretation_Tm_refine_b582da5b18980dd549f83acfd27b47df" ], 0, - "5a6f45a6e81f162513460535ec463076" + "24c6fdcbe50d55cee831fb263a7dff5d" ], [ "LowStar.Lib.AssocList.add", @@ -340,7 +340,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "04a65a80bf67d4495414cfd4f750fd8c" + "dc7084ad5e2f9b5e6c2720169046bdb9" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -352,7 +352,7 @@ "refinement_interpretation_Tm_refine_666cbc765faa85ecb6368ba0ccf434cd" ], 0, - "ad637e7f0cc1574c903662df8c5ab4d7" + "083e0e3668db7d7644107014280fe8fb" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -481,7 +481,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "42ca71afa5355c63ba844ceb015feb73" + "5d9f5d118f97d249132a4e9a9c6fe8ef" ], [ "LowStar.Lib.AssocList.remove_all", @@ -593,7 +593,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "4e15935e1b90e91a787d73287ef94d4d" + "fc4b661fd6b0ced039a6e5adff6add4b" ], [ "LowStar.Lib.AssocList.clear", @@ -680,7 +680,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "dad0c6f95a95a12a178c2e2b4674fd23" + "ede67cb419bc4978ab8e97c106097e27" ], [ "LowStar.Lib.AssocList.free", @@ -752,7 +752,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "34a0c373fd49740e0586e7efee2d4fb9" + "4e426cec870f2473ba61cee504805bc6" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints index 6443034a..f9238255 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints @@ -15,7 +15,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "44cf23ba4f51019ddf7e1ee9367f3b70" + "a43235b13f77c68e1ecba07a72f606c9" ], [ "LowStar.Lib.LinkedList.cells", @@ -43,7 +43,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "dda12eec094f7388aff40300859bed80" + "3cb7d8f4f30c58a7e0cc34e840a63b70" ], [ "LowStar.Lib.LinkedList.same_cells_same_pointer", @@ -79,7 +79,7 @@ "unit_typing" ], 0, - "84ae6abfabcf47b2c53e76beca18c3b0" + "cf99570ce3677413c6a052cbb618c399" ], [ "LowStar.Lib.LinkedList.footprint", @@ -107,7 +107,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "7b05dcf906e6026d196cd040ea8bed00" + "8fe483b36b66962b7b57dd19c5c0fb94" ], [ "LowStar.Lib.LinkedList.cells_pairwise_disjoint", @@ -137,7 +137,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "35096efc405de285c33ba29d644d27a1" + "94e3fe4d3ae31d46bcf51231bd52d93d" ], [ "LowStar.Lib.LinkedList.cells_live_freeable", @@ -167,7 +167,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "e34b7a0fc13c0bd7ab63de59d290b447" + "bc18ec597bd9633eb042fc601fe51eda" ], [ "LowStar.Lib.LinkedList.invariant", @@ -176,7 +176,7 @@ 1, [ "@query", "equation_Prims.logical" ], 0, - "96888138661153d5d1594d47dfb8e646" + "0d54fb0fd2c4a5bad5af165a98e84f11" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -234,7 +234,7 @@ "typing_LowStar.Monotonic.Buffer.loc_not_unused_in" ], 0, - "51d23a81582ffb4376dc57cea8555efa" + "93542818fc850b2208f0c5cd8b3fa4c9" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -248,7 +248,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "af71849a753a268944d47a5c63ef203e" + "83aab2f482e38218e21212131ce739de" ], [ "LowStar.Lib.LinkedList.frame", @@ -339,7 +339,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "06f8d6f24a8bfe104c084ff7bce2433c" + "328a9846c7d94732ada0611ad8f301c6" ], [ "LowStar.Lib.LinkedList.frame", @@ -351,7 +351,7 @@ "refinement_interpretation_Tm_refine_9dfd5ec664d04b1adbe6909975d3119f" ], 0, - "d71ba7bd9f5f9c19f0d00b86573b06a8" + "c3c04347d8d2ce9363510f56e080c31b" ], [ "LowStar.Lib.LinkedList.length_functional", @@ -389,7 +389,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "bd23e7b6889d311b2866c20bf3cbd09e" + "072da938e14aa723b062b50fb2ed2e8f" ], [ "LowStar.Lib.LinkedList.gmap", @@ -404,7 +404,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "91459d89d7a6cba94f303c887edd4302" + "d0fdabc39fd8ee12d6024e88812fe380" ], [ "LowStar.Lib.LinkedList.gfold_right", @@ -419,7 +419,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "2c38747c4993d8c4709d094f37377966" + "fc1cb9b4ddac1834506d85d55482123a" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -483,7 +483,7 @@ "typing_LowStar.Lib.LinkedList.cells" ], 0, - "4b1858a25beabe31706242943ca1cb7a" + "56b7bcb240be7e88108d15a847c5b2b3" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -495,7 +495,7 @@ "refinement_interpretation_Tm_refine_2cdb1d22d11cea5954bcab0f89d645ec" ], 0, - "15bf014c22870a2aa3a698ad91ee593e" + "e37827525e3280c4de1ea8817f96b49a" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -577,7 +577,7 @@ "typing_Tm_abs_f132d2aafff03dbbf3f24162269a2dac" ], 0, - "60cdb4e04b322da821f9fd769d7e21aa" + "087353052938d79b248d163a8ffb0414" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -591,7 +591,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "1ecac629f888a68c31dcd639d06cec25" + "a3afa0a11b03eb40b872872c7651dfb8" ], [ "LowStar.Lib.LinkedList.push", @@ -603,7 +603,7 @@ "refinement_interpretation_Tm_refine_2e3312cd41d7f5efbbbae3b2eeef697e" ], 0, - "dd228f84aa9041902b73a41fe9bced5c" + "54400e3c86a5101623042fd841595a92" ], [ "LowStar.Lib.LinkedList.push", @@ -729,7 +729,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "a8050fc97f5d06fa24b09a70492b8395" + "7c9520d590702fc4b0325cae5464aabf" ], [ "LowStar.Lib.LinkedList.pop", @@ -760,7 +760,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "c84bf47b30fb08e0bcce1c005f37eb25" + "8d75e376e9de3de44254a2c6cb218adc" ], [ "LowStar.Lib.LinkedList.pop", @@ -868,7 +868,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "0e20212aff4b9f0e5c82938b57b86789" + "6c47aaf0f23763d618be1bc833eda030" ], [ "LowStar.Lib.LinkedList.free_", @@ -880,7 +880,7 @@ "refinement_interpretation_Tm_refine_994dd8cb51034b7a0776f9bb28ca6f71" ], 0, - "e0d21b6058fa87afa6c2529d754bd9df" + "627c8b8ef83de9926b95814612ce95aa" ], [ "LowStar.Lib.LinkedList.free_", @@ -970,7 +970,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "53779c3448f2a1f7da74553f5936def0" + "5b7a5f34f2589ece6677e93e47411a56" ], [ "LowStar.Lib.LinkedList.free", @@ -982,7 +982,7 @@ "refinement_interpretation_Tm_refine_baa6a0434e5b51218cc000deadc8f6bc" ], 0, - "1923b5789609b8299ee05bb369035d15" + "aa003a0a00a77fe333a49d4de431cb80" ], [ "LowStar.Lib.LinkedList.free", @@ -1069,7 +1069,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "0d71c23b88a135da0aed2f88130acd6f" + "257cd507ddcab9d8e673ed8fc588de57" ], [ "LowStar.Lib.LinkedList.length", @@ -1078,7 +1078,7 @@ 1, [ "@query" ], 0, - "92cd6abf727a633f8a20161e3e7a2f64" + "ed6a90b2de6d563afa37a81e6f90960f" ], [ "LowStar.Lib.LinkedList.length", @@ -1137,7 +1137,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "c592cb16d0fbf3ce20beeaf2315cfd02" + "b98749a19696f09bc31edee4d231ce13" ], [ "LowStar.Lib.LinkedList.test", @@ -1274,7 +1274,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "7340780c836de142906348b92b5688a5" + "9599f436947472e3e3aff6ae3661b11a" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints index b77c9f8e..ceba8ee3 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints @@ -17,7 +17,7 @@ "typing_LowStar.Lib.LinkedList2.__proj__Mkt__item__r" ], 0, - "28ee7a81d7fcf80718ba40dad0506572" + "76727c9c6bcbf23c3dbb42371812582c" ], [ "LowStar.Lib.LinkedList2.footprint", @@ -29,7 +29,7 @@ "l_and-interp" ], 0, - "00441062e79667099f0bb50437d4567c" + "10b9b437735b1d0c11ed76bc9ee364b5" ], [ "LowStar.Lib.LinkedList2.cells", @@ -41,7 +41,7 @@ "l_and-interp" ], 0, - "921c578bf6310a949fbdf2bc1e75fa1a" + "4ae9327f390a96dfea85dccd7cfa94b6" ], [ "LowStar.Lib.LinkedList2.footprint_in_r", @@ -111,7 +111,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "8c41e9a42511d2a052fc82168a2b2a32" + "5876598890f7b31675c3d8de530e4ebc" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -123,7 +123,7 @@ "refinement_interpretation_Tm_refine_09ad67b9d90ed7b17ddf31c45c68b636" ], 0, - "37cea3975a89a28885bf88736a4c88c7" + "c260141341e49d7e6594888f2815d97d" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -183,7 +183,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "7a3223a1119aa0e7d90a1849d689ddc2" + "b3f7a42fc6a854b69f50a332909fa38e" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -195,7 +195,7 @@ "refinement_interpretation_Tm_refine_76a8d76aec5fe95490cf6c28517bab40" ], 0, - "d3e6925f2431350de9d925a214bc5aad" + "2571776695e97d2f592056bb10f742c1" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -256,7 +256,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "3967096f04dbc7a283ebf04361152ccb" + "b1ac32e48cc9dd5e2052948e65f8e738" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -265,7 +265,7 @@ 0, [ "@query" ], 0, - "769d643d5ea388b85eeb4d3b976a4495" + "3c71f773c73407dfb7eac15726c670f5" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -396,7 +396,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "17b99853d9501f8997a23352e4b92ac5" + "f76a92ec990946103acbff1415af3dce" ], [ "LowStar.Lib.LinkedList2.push", @@ -408,7 +408,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "d680932218091448eccb478c46ced68d" + "0dcd5aef8f717c3479900683af5c6973" ], [ "LowStar.Lib.LinkedList2.push", @@ -525,7 +525,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "da436a3c7e2178a002599f91dfec1cfb" + "6e1249b0030c140a7e912953d809fd55" ], [ "LowStar.Lib.LinkedList2.pop", @@ -571,7 +571,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "3dcde12d996050ede57e4b26eb343fe1" + "12aa4a9edec96250002601a88cbcbeb3" ], [ "LowStar.Lib.LinkedList2.pop", @@ -694,7 +694,7 @@ "typing_Prims.uu___is_Cons" ], 0, - "cc89dda6781386306ea173836a065ac7" + "c38db77aff2fbeda94428478c51fd9a5" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -743,7 +743,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "608b70f1b4a74165ccd6bcfef7df4077" + "bd0cebbee5f4efb3083f65fed3febfd5" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -883,7 +883,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "bcd0ff1bf0d9b61695cf2c0f0ba3a429" + "fedb8ff0ffd1d2bd7289194f063a2aa6" ], [ "LowStar.Lib.LinkedList2.clear", @@ -895,7 +895,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "77240ba36fe062476abdccd742693c10" + "2c0075cc9f19ba39178adf144614207b" ], [ "LowStar.Lib.LinkedList2.clear", @@ -1006,7 +1006,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "b74a4a40b7fa110cb38280ae8f3bf654" + "768f9a16a3652e3086d343c31f3be41a" ], [ "LowStar.Lib.LinkedList2.free", @@ -1018,7 +1018,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "6562bfb1cc24221953d950b9b78611ab" + "dc9d45602aa0eaa7c281d951e508e75e" ], [ "LowStar.Lib.LinkedList2.free", @@ -1097,7 +1097,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "6ae80714e3c601b213b5bb9a0c642db6" + "faa197dea80936a25ae41bc6f5da8337" ], [ "LowStar.Lib.LinkedList2.test", @@ -1234,7 +1234,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "5a885ba3dde44eaad5769e331a31107d" + "fef24972074138e1e68bc1f823b1c55f" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/Spec.Loops.fst.hints b/krmllib/hints/Spec.Loops.fst.hints index ecefac61..06448385 100644 --- a/krmllib/hints/Spec.Loops.fst.hints +++ b/krmllib/hints/Spec.Loops.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "81e898ae20210955d704b7cc2fc1c8ac" + "456bb65917231789baac5b4274ab78a1" ], [ "Spec.Loops.seq_map", @@ -57,7 +57,7 @@ "well-founded-ordering-on-nat" ], 0, - "81272493f59fb3c2a1e06360370c0f70" + "f00f7f594b7833e9455d2bbe8793ba22" ], [ "Spec.Loops.seq_map", @@ -71,7 +71,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "6871cb2838ce92844d1d67d9fc9d00be" + "b7dc3cfa48bcee6035ef530a590c7eeb" ], [ "Spec.Loops.seq_map2", @@ -86,7 +86,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "8550e35640cb828b65e1f483c8a87513" + "110c113758e6b2329f53d3f760adaef6" ], [ "Spec.Loops.seq_map2", @@ -133,7 +133,7 @@ "well-founded-ordering-on-nat" ], 0, - "5778ef5443ac13a9b7ec1104506da1ee" + "9921a35d3d9d231c5d61174cbfe41692" ], [ "Spec.Loops.seq_map2", @@ -148,7 +148,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "2c653006b18fb77143eacc58b376c92c" + "96e7457edc28466bf8b35129f7857005" ], [ "Spec.Loops.repeat", @@ -164,7 +164,7 @@ "well-founded-ordering-on-nat" ], 0, - "c1867c77ac98c123980962be3bf523bc" + "8f9ca37edf49a1165646713da69d3de6" ], [ "Spec.Loops.repeat_induction", @@ -177,7 +177,7 @@ "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001" ], 0, - "0dfc3fc072602e2cb07f2b64a4259076" + "54645fdce13fc74cb792eed7316733af" ], [ "Spec.Loops.repeat_induction", @@ -206,7 +206,7 @@ "typing_Spec.Loops.repeat", "well-founded-ordering-on-nat" ], 0, - "b611bf42d881f193949d2a67ee4170d6" + "ad6acb160a13a7aed1a7b5ba973367c4" ], [ "Spec.Loops.repeat_induction", @@ -219,7 +219,7 @@ "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001" ], 0, - "76d635ee1e3f36c0eaaa78f961304c66" + "911c17cb862d2f95871a3d82390340e1" ], [ "Spec.Loops.repeat_base", @@ -242,7 +242,7 @@ "refinement_interpretation_Tm_refine_f52d524f7d227b5c40129c018d34fe1d" ], 0, - "f6c5b24cb721108513a6da6132e9ac15" + "3011c3f4e907689e6585d839fc839013" ], [ "Spec.Loops.repeat_range", @@ -267,7 +267,7 @@ "well-founded-ordering-on-nat" ], 0, - "ea617c8b20fdaa5127ba6be201dd70f2" + "6114defb8cb62685dfac0e15d01627c7" ], [ "Spec.Loops.repeat_range_base", @@ -276,7 +276,7 @@ 1, [ "@query" ], 0, - "ca91d160c752c2fc9bf77328cb364ad4" + "09fa0e8117809913b8a27899916a5099" ], [ "Spec.Loops.repeat_range_base", @@ -293,7 +293,7 @@ "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913" ], 0, - "fad6856f05e0b49b9a3475e42854a490" + "18ed30f45f68240f9898fe767f7b769b" ], [ "Spec.Loops.repeat_range_induction", @@ -308,7 +308,7 @@ "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79" ], 0, - "c7129aebb2c5e8bb17fef8c433b2aabd" + "e64a208d48b6f1069444978eda2b25e2" ], [ "Spec.Loops.repeat_range_induction", @@ -341,7 +341,7 @@ "typing_Spec.Loops.repeat_range", "well-founded-ordering-on-nat" ], 0, - "b27a7a2923b1a682bf9320db7cf12f9f" + "22590f8a6de8b9720e7d584e7737ffa3" ], [ "Spec.Loops.repeat_range_induction", @@ -356,7 +356,7 @@ "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79" ], 0, - "6cc3ec6279682b6f449bcd7a910a7e66" + "2c55389a00c97e4a2c95b39fdaf7db7b" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/TestLib.fsti.hints b/krmllib/hints/TestLib.fsti.hints index 0519c0e0..fb698a30 100644 --- a/krmllib/hints/TestLib.fsti.hints +++ b/krmllib/hints/TestLib.fsti.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "f898b2493d5d796fba5504f1f139d392" + "4ee98b59aa0bfe01ef141cbc7e272ce4" ], [ "TestLib.unsafe_malloc", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "d7c3c3f16c6eeacb8c3fcbb1a46de372" + "df857d023f8e2ef0ffc6fa93829a8d9f" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/WasmSupport.fst.hints b/krmllib/hints/WasmSupport.fst.hints index 6a10cd83..2c0d3c66 100644 --- a/krmllib/hints/WasmSupport.fst.hints +++ b/krmllib/hints/WasmSupport.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "be22e741df12626f5235b163d81864c7" + "8eb00e1371a59b64833b91203a39c48a" ], [ "WasmSupport.betole64", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "b2fceec1c4cb5f2e5b9b0bd59fe78539" + "8656cce09621cd11afccdbb28d7c2cc7" ], [ "WasmSupport.memzero", @@ -63,7 +63,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "938864ff5429d7f2fca742ce8f7c6da4" + "cb5132b049334a10e85c8cc81b4b17ad" ] ] ] \ No newline at end of file diff --git a/lib/Ast.ml b/lib/Ast.ml index afdeaf10..776e8a36 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -26,6 +26,7 @@ and width = K.width [@ visitors.opaque] and lifetime = Common.lifetime [@ visitors.opaque] and constant = K.t [@ visitors.opaque] and ident = string [@ visitors.opaque] +and z = Z.t [@ opaque] and poly_comp = K.poly_comp [@ visitors.opaque] [@ show.opaque] and forward_kind = Common.forward_kind [@ visitors.opaque] and lident = ident list * ident [@ visitors.opaque] @@ -104,7 +105,7 @@ and type_def = | Abbrev of typ | Flat of fields_t_opt | Variant of branches_t - | Enum of (lident * int option) list + | Enum of (lident * z option) list | Union of (ident * typ) list | Forward of forward_kind diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml index d67c6de5..1b98906e 100644 --- a/lib/AstToCFlat.ml +++ b/lib/AstToCFlat.ml @@ -356,9 +356,9 @@ let populate env files = if List.exists (fun (_, v) -> v <> None) idents then assert (List.for_all (fun (_, v) -> v <> None) idents); KList.fold_lefti (fun i env (ident, v) -> - let i = Option.value ~default:i v in - assert (i < 256); - { env with enums = LidMap.add ident i env.enums } + let i = Option.value ~default:(Z.of_int i) v in + assert (Z.lt i (Z.of_int 256)); + { env with enums = LidMap.add ident (Z.to_int i) env.enums } ) env idents | _ -> env diff --git a/lib/C11.ml b/lib/C11.ml index 14f12359..4de8af4d 100644 --- a/lib/C11.ml +++ b/lib/C11.ml @@ -14,7 +14,7 @@ type type_spec = (** Note: the option allows for zero-sized structs (GCC's C, C++) but as * of 2017/05/14 we never generate these. *) | Union of ident option * declaration list option - | Enum of ident option * (ident * int option) list + | Enum of ident option * (ident * Ast.z option) list (** not encoding all the invariants here *) [@@deriving show] diff --git a/lib/CStar.ml b/lib/CStar.ml index a4db9acc..6917161d 100644 --- a/lib/CStar.ml +++ b/lib/CStar.ml @@ -119,7 +119,7 @@ and typ = | Bool | Struct of (ident option * typ) list (** In support of anonymous unions. *) - | Enum of (lident * int option) list + | Enum of (lident * Ast.z option) list | Union of (ident * typ) list | Const of typ (* note: when we have restrict, or MinLength, extend this to be a diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml index 8d6c6f5e..12125d84 100644 --- a/lib/CStarToC11.ml +++ b/lib/CStarToC11.ml @@ -1136,10 +1136,14 @@ let wrap_verbatim lid flags d = [] let enum_as_macros cases = + (* Since enums do not support arithmetic operations, we have no issues with + integer promotion and need not concern ourselves with suffixes or e.g. a + constant being promoted to a large signed type unintentionally. *) let lines: string list = List.mapi (fun i (c, v) -> match v with | None -> KPrint.bsprintf "#define %s %d" c i - | Some i -> KPrint.bsprintf "#define %s %d" c i + | Some v -> + KPrint.bsprintf "#define %s %s" c (Z.to_string v) ) cases in String.concat "\n" lines @@ -1287,22 +1291,36 @@ let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.decl | Enum cases when !Options.short_enums -> (* Note: EEnum translates as just a name -- so we don't have to * change use-sites, they directly resolve as the macro. *) + let max_value, min_value = + let custom_values = List.filter_map snd cases in + let custom_values = List.sort compare custom_values in + print_endline (String.concat ", " (List.map Z.to_string custom_values)); + max + (* conservative if we allow signed values *) + (if custom_values <> [] then KList.last custom_values else Z.zero) + (Z.of_int (List.length cases)), + if custom_values <> [] then List.hd custom_values else Z.zero + in + KPrint.bprintf "max_value=%s, min_value=%s\n" (Z.to_string max_value) (Z.to_string min_value); let t = - if List.length cases <= 0xff && List.for_all (function (_, Some i) -> i <= 0xff | _ -> true) cases then + if Z.(geq min_value zero && leq max_value (of_string "0xff")) then K.UInt8 - else if List.length cases <= 0xffff && List.for_all (function (_, Some i) -> i <= 0xffff | _ -> true) cases then + else if Z.(geq min_value zero && leq max_value (of_string "0xffff")) then K.UInt16 + else if Z.(geq min_value zero && leq max_value (of_string "0xffffffff")) then + K.UInt32 + else if Z.(geq min_value zero && leq max_value (of_string "0xffffffffffffffff")) then + K.UInt64 + else if Z.(geq min_value (of_string "-0x7e") && leq max_value (of_string "0x7f")) then + K.Int8 + else if Z.(geq min_value (of_string "-0x7ffe") && leq max_value (of_string "0x7fff")) then + K.Int16 + else if Z.(geq min_value (of_string "-0x7ffffffe") && leq max_value (of_string "0x7fffffff")) then + K.Int32 + else if Z.(geq min_value (of_string "-0x7ffffffffffffffe") && leq max_value (of_string "0x7fffffffffffffff")) then + K.Int64 else - let l = List.length cases in - let cmp x y = - match x, y with - | (_, Some x), (_, Some y) -> compare x y - | (_, Some _), _ -> 1 - | _, (_, Some _) -> -1 - | _ -> 0 - in - let max = match snd (List.hd (List.sort cmp cases)) with Some v -> string_of_int v | None -> "None" in - failwith (KPrint.bsprintf "Too many cases for enum %s: %d cases, max is %s" name l max) + failwith "TODO: support for negative enum values" in let cases = List.map (fun (lid, v) -> to_c_name m lid, v) cases in wrap_verbatim name flags (Text (enum_as_macros cases)) @ diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml index 6faf755d..d13279cc 100644 --- a/lib/DataTypes.ml +++ b/lib/DataTypes.ml @@ -326,7 +326,7 @@ let allocate_tag enums preferred_lid tags = let field_for_tag = "tag" let field_for_union = "val" -type map = (lident, scheme) Hashtbl.t * ((lident * int option) list, lident) Hashtbl.t +type map = (lident, scheme) Hashtbl.t * ((lident * Z.t option) list, lident) Hashtbl.t (* This does two things: * - deal with the simple compilation schemes (not tagged union) diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml index b62604f1..e4f4be4a 100644 --- a/lib/PrintAst.ml +++ b/lib/PrintAst.ml @@ -13,6 +13,8 @@ open Common let arrow = string "->" let lambda = fancystring "λ" 1 +let z x = string (Z.to_string x) + let print_app_ empty f head g arguments = group ( f head ^^ jump ( @@ -92,7 +94,7 @@ and print_type_def = function braces_with_nesting (separate_map (comma ^^ break1) (fun (lid, value) -> string (string_of_lident lid) ^^ match value with | None -> empty - | Some value -> space ^^ equals ^^ break1 ^^ int value + | Some value -> space ^^ equals ^^ break1 ^^ z value ) tags) | Union fields -> diff --git a/lib/PrintC.ml b/lib/PrintC.ml index edce22d2..d257cf92 100644 --- a/lib/PrintC.ml +++ b/lib/PrintC.ml @@ -86,7 +86,18 @@ let rec p_type_spec = function group (string "enum" ^/^ (match name with Some name -> string name ^^ break1 | None -> empty)) ^^ braces_with_nesting (separate_map (comma ^^ break1) (fun (id, v) -> - string id ^^ match v with None -> empty | Some v -> space ^^ equals ^^ space ^^ int v + let suffix = + match v with + | Some v -> + (* Some notes. 1) Must Z.of_string in the unlikely event that krml is running on a + 32-bit machine. 2) This assert may be tripped as there is currently no code to + automatically decline -fenum for constants that don't fit. 3) *) + if not Z.(leq v (of_string "0xffffffff") && gt v (of_string "-0xffffffff")) then + failwith ("Cannot use C11 enum for " ^ Option.value ~default:"???" name ^ " since the value of one of the constants may exceed the size of int"); + space ^^ equals ^^ space ^^ PrintAst.z v + | None -> empty + in + string id ^^ suffix ) tags) and p_qualifier = function From 31f75b386d3f2c42872b4e32cb8c5ad303a2d0f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 8 Jan 2025 19:39:34 -0800 Subject: [PATCH 2/2] install-deps: fix standalone CI Path to script was wrong, causing a confusing error with sudo --- .docker/build/install-deps.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.docker/build/install-deps.sh b/.docker/build/install-deps.sh index 539b51e9..ecbbbaaa 100755 --- a/.docker/build/install-deps.sh +++ b/.docker/build/install-deps.sh @@ -19,7 +19,7 @@ git clone --branch $FSTAR_BRANCH https://github.com/FStarLang/FStar "$FSTAR_HOME opam install --deps-only "$FSTAR_HOME/fstar.opam" OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$FSTAR_HOME" -sudo "$FSTAR_HOME/bin/get_fstar_z3.sh" "/usr/local/bin" +sudo "$FSTAR_HOME/.scripts/get_fstar_z3.sh" "/usr/local/bin" # Install other deps "$build_home"/install-other-deps.sh