From 548a6eadced0f0f727bd0381bb8d4c39960bcd8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20Rieu-Helft?= Date: Wed, 9 Nov 2016 17:01:59 +0100 Subject: [PATCH] Module Main now compiles --- drivers/c.drv | 20 +- examples/in_progress/multiprecision/mp2.mlw | 63 +++- .../multiprecision/mp2/why3session.xml | 105 ++++-- .../in_progress/multiprecision/mp2/why3shapes | 29 +- modules/mach/c.mlw | 20 ++ src/mlw/cprinter.ml | 337 ++++++++++-------- 6 files changed, 375 insertions(+), 199 deletions(-) diff --git a/drivers/c.drv b/drivers/c.drv index e299edd84..df036bd7f 100644 --- a/drivers/c.drv +++ b/drivers/c.drv @@ -1,9 +1,13 @@ - printer "c" module ref.Ref syntax type ref "%1" + syntax val ref "%1" + syntax converter ref "%1" + syntax val (!_) "%1" + syntax converter (!_) "%1" + syntax val (:=) "%1 = %2" end @@ -55,7 +59,10 @@ end module mach.c.C - syntax type ptr "(%1 *)" + prelude "#include " + prelude "#include " + + syntax type ptr "%1 *" syntax val malloc "malloc(%1 * sizeof(%v0))" (* and not %t1 ? *) syntax val free "free(%1)" @@ -64,10 +71,19 @@ module mach.c.C syntax val is_null "%1 == NULL" syntax val null "NULL" + syntax val incr "%1+%2" + syntax val get "*(%1)" syntax val set "*(%1) = %2" syntax val p2i "%1" syntax converter p2i "%1" + syntax val break "break" + syntax val return32 "return (%1)" + + syntax val print_space "printf(\" \")" + syntax val print_newline "printf(\"\\n\")" + syntax val print_uint32 "printf(\"%#x\",%1)" + end \ No newline at end of file diff --git a/examples/in_progress/multiprecision/mp2.mlw b/examples/in_progress/multiprecision/mp2.mlw index 2ba1e5ad7..6c040497f 100644 --- a/examples/in_progress/multiprecision/mp2.mlw +++ b/examples/in_progress/multiprecision/mp2.mlw @@ -199,8 +199,6 @@ module N ensures { c * a < c * b } = () - exception Break32 int32 - use import ref.Refint function compare_int (x y:int) : int = @@ -275,13 +273,13 @@ module N }; res := Int32.of_int (-1) end; - raise Break32 !res + return32 !res; end else () done; value_sub_frame_shift (pelts x) (pelts y) x.offset y.offset (p2i sz); zero - with Break32 r -> r + with Return32 r -> r end (* [is_zero] checks if [x[0..sz-1]] is zero. It corresponds to [mpn_zero_p]. *) @@ -307,14 +305,14 @@ module N value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz); value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k); value_sub_lower_bound (pelts x) (x.offset+k) (x.offset + p2i sz); - raise Break32 (Int32.of_int 0) + return32 (Int32.of_int 0); end else begin assert { 1+2=3 }; end done; Int32.of_int 1 - with Break32 r -> r + with Return32 r -> r end (** [zero r sz] sets [(r,sz)] to zero. Corresponds to [mpn_zero]. *) @@ -335,8 +333,6 @@ module N (** {2 Addition} *) - exception Break - (** [add_limb r x y sz] adds to [x] the value of the limb [y], writes the result in [r] and returns the carry. [r] and [x] have size [sz]. This corresponds to the function [mpn_add_1] *) @@ -2112,24 +2108,71 @@ module N assert { l2i !qh * l2i d + l2i !r = l2i ul + radix * l2i uh }; (!qh,!r) - end module Main use import mach.c.C use import N + use import mach.int.Int32 + use import int.Int + use import ref.Ref + + let print (p:t) (m n:int32) : unit + requires { 0 <= p.offset + p2i m + <= p.offset + p2i n + <= plength p } + = + let i = ref m in + let q = ref (incr p m) in + let one = Int32.of_int 1 in + while (Int32.(<) !i n) do + invariant { p2i m <= p2i !i <= p2i n } + invariant { (!q).offset = p.offset + p2i !i } + invariant { plength !q = plength p } + variant { p2i n - p2i !i } + print_uint32 (get !q); + print_space (); + q := C.incr !q one; + i := Int32.(+) !i one; + done; + print_newline () let from_limb (l:limb) : t ensures { is_null result \/ plength result = 1 } ensures { is_null result \/ value_sub_shift result 1 = l2i l } + ensures { result.offset = 0 } = let p = malloc (UInt32.of_int 1) in if not (is_null p) then C.set p l; p - let main () = from_limb (Limb.of_int 42) + let two_limbs (l1 l2: limb) : t + ensures { is_null result \/ plength result = 2 } + ensures { is_null result \/ value_sub_shift result 2 = l2i l1 + radix * l2i l2 } + ensures { result.offset = 0 } + = + let p = malloc (UInt32.of_int 2) in + if not (is_null p) + then begin + C.set p l1; + C.set (incr p (Int32.of_int 1)) l2 + end; + p + + let main () = + let p = from_limb (Limb.of_int 42) in + if not (is_null p) + then begin + print_uint32 (get p); + print_newline (); + end; + free p; + let q = two_limbs (Limb.of_int 42) (Limb.of_int 28) in + if not (is_null q) + then print q (Int32.of_int 0) (Int32.of_int 2); + free q; end diff --git a/examples/in_progress/multiprecision/mp2/why3session.xml b/examples/in_progress/multiprecision/mp2/why3session.xml index 147800405..f25357863 100644 --- a/examples/in_progress/multiprecision/mp2/why3session.xml +++ b/examples/in_progress/multiprecision/mp2/why3session.xml @@ -10,7 +10,7 @@ - + @@ -277,47 +277,65 @@ - + + + + + + + + + + - + - + - + - + - + - + - + - + + + + + + + + + + - + - + - + - + - + @@ -358,31 +376,40 @@ - + + + + + + + + + + - - + + - + - + - + - + - + - + - + @@ -1692,10 +1719,10 @@ - + - + @@ -2274,10 +2301,10 @@ - + - + @@ -2862,7 +2889,6 @@ - @@ -3999,7 +4025,7 @@ - + @@ -4015,15 +4041,28 @@ - + + + + + + + - + + + + + + + + diff --git a/examples/in_progress/multiprecision/mp2/why3shapes b/examples/in_progress/multiprecision/mp2/why3shapes index 22ee1f72c..7517dd694 100644 --- a/examples/in_progress/multiprecision/mp2/why3shapes +++ b/examples/in_progress/multiprecision/mp2/why3shapes @@ -58,7 +58,7 @@ dffa7670276df3f668d6b159221ea268 VC for value_sub_upper_bound_tightainfix apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV0ainfix -V17c1avalue_sub_shiftV1ainfix -V17c1Aainfix >=ainfix *ainfix -al2iV22al2iV21apoweraradixainfix -V17c1apoweraradixainfix -V17c1Aainfix =ainfix -avalue_sub_shiftV1V17avalue_sub_shiftV0V17ainfix -ainfix *ainfix -al2iV22al2iV21apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV0ainfix -V17c1avalue_sub_shiftV1ainfix -V17c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V17c1Iainfix al2iV22al2iV21ainfix =ap2iV47acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2Iainfix =V47V46FIainfix =ato_intV46c1FAain_boundsc1Aainfix >apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV1ainfix -V17c1avalue_sub_shiftV0ainfix -V17c1Aainfix >=ainfix *ainfix -al2iV21al2iV22apoweraradixainfix -V17c1apoweraradixainfix -V17c1Aainfix =ainfix -avalue_sub_shiftV0V17avalue_sub_shiftV1V17ainfix -ainfix *ainfix -al2iV21al2iV22apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV1ainfix -V17c1avalue_sub_shiftV0ainfix -V17c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V17c1Iainfix ato_intV21ato_intV22Iainfix =avalue_subV38V37ainfix +V36c1ainfix +avalue_subV38V37V36ainfix *al2iagetV38V36apoweraradixainfix -V36V37Aainfix <=V37V36LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V17c1Iainfix =avalue_subV35V34ainfix +V33c1ainfix +avalue_subV35V34V33ainfix *al2iagetV35V33apoweraradixainfix -V33V34Aainfix <=V34V33LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V17c1Aainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V17avalue_sub_shiftV1V17Iainfix =avalue_subV32V31V29ainfix +avalue_subV32V31V30ainfix *avalue_subV32V30V29apoweraradixainfix -V30V31Aainfix <=V30V29Aainfix <=V31V30LapeltsV1LaoffsetV1Lainfix +aoffsetV1V17Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV28V27V25ainfix +avalue_subV28V27V26ainfix *avalue_subV28V26V25apoweraradixainfix -V26V27Aainfix <=V26V25Aainfix <=V27V26LapeltsV0LaoffsetV0Lainfix +aoffsetV0V17Lainfix +aoffsetV0ato_intV2ainfix =V23aTrueINainfix =ato_intV21ato_intV22Iainfix =V23aTrueAainfix =V23aTrueINainfix =V21V22FIainfix =V22amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV20FAainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FAain_boundsc1Iainfix =amixfix []apeltsV0ainfix +aoffsetV0V50amixfix []apeltsV1ainfix +aoffsetV1V50Iainfix apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV0ainfix -V17c1avalue_sub_shiftV1ainfix -V17c1Aainfix >=ainfix *ainfix -al2iV22al2iV21apoweraradixainfix -V17c1apoweraradixainfix -V17c1Aainfix =ainfix -avalue_sub_shiftV1V17avalue_sub_shiftV0V17ainfix -ainfix *ainfix -al2iV22al2iV21apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV0ainfix -V17c1avalue_sub_shiftV1ainfix -V17c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V17c1Iainfix al2iV22al2iV21ainfix =ap2iV50acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2Iainfix =V49V50FAainfix apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV1ainfix -V17c1avalue_sub_shiftV0ainfix -V17c1Aainfix >=ainfix *ainfix -al2iV21al2iV22apoweraradixainfix -V17c1apoweraradixainfix -V17c1Aainfix =ainfix -avalue_sub_shiftV0V17avalue_sub_shiftV1V17ainfix -ainfix *ainfix -al2iV21al2iV22apoweraradixainfix -V17c1ainfix -avalue_sub_shiftV1ainfix -V17c1avalue_sub_shiftV0ainfix -V17c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V17c1Iainfix ato_intV21ato_intV22Iainfix =avalue_subV38V37ainfix +V36c1ainfix +avalue_subV38V37V36ainfix *al2iagetV38V36apoweraradixainfix -V36V37Aainfix <=V37V36LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V17c1Iainfix =avalue_subV35V34ainfix +V33c1ainfix +avalue_subV35V34V33ainfix *al2iagetV35V33apoweraradixainfix -V33V34Aainfix <=V34V33LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V17c1Aainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V17avalue_sub_shiftV1V17Iainfix =avalue_subV32V31V29ainfix +avalue_subV32V31V30ainfix *avalue_subV32V30V29apoweraradixainfix -V30V31Aainfix <=V30V29Aainfix <=V31V30LapeltsV1LaoffsetV1Lainfix +aoffsetV1V17Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV28V27V25ainfix +avalue_subV28V27V26ainfix *avalue_subV28V26V25apoweraradixainfix -V26V27Aainfix <=V26V25Aainfix <=V27V26LapeltsV0LaoffsetV0Lainfix +aoffsetV0V17Lainfix +aoffsetV0ato_intV2ainfix =V23aTrueINainfix =ato_intV21ato_intV22Iainfix =V23aTrueAainfix =V23aTrueINainfix =V21V22FIainfix =V22amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV20FAainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FAain_boundsc1Iainfix =amixfix []apeltsV0ainfix +aoffsetV0V54amixfix []apeltsV1ainfix +aoffsetV1V54Iainfix apoweraradixainfix -V12c1ainfi df186c0c70a74fa062e067f625628a3d VC for compare_same_sizeainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V39amixfix []apeltsV1ainfix +aoffsetV1V39Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V39amixfix []apeltsV1ainfix +aoffsetV1V39Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V40amixfix []apeltsV1ainfix +aoffsetV1V40Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V39amixfix []apeltsV1ainfix +aoffsetV1V39Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV0V12avalue_sub_shiftV1V12ainfix -ainfix *ainfix -al2iV16al2iV17apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV1ainfix -V12c1avalue_sub_shiftV0ainfix -V12c1Iainfix <=c0avalue_subapeltsV0aoffsetV0ainfix -ainfix +aoffsetV0V12c1Iainfix ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V40amixfix []apeltsV1ainfix +aoffsetV1V40Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V35amixfix []apeltsV1ainfix +aoffsetV1V35Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfi 17a3414eb42d2f18aa1e45536791cc32 VC for compare_same_sizeainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V37amixfix []apeltsV1ainfix +aoffsetV1V37Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V38amixfix []apeltsV1ainfix +aoffsetV1V38Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V40amixfix []apeltsV1ainfix +aoffsetV1V40Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V40amixfix []apeltsV1ainfix +aoffsetV1V40Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V41amixfix []apeltsV1ainfix +aoffsetV1V41Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V40amixfix []apeltsV1ainfix +aoffsetV1V40Iainfix apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Aainfix >=ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1apoweraradixainfix -V12c1Iainfix =ainfix -avalue_sub_shiftV1V12avalue_sub_shiftV0V12ainfix -ainfix *ainfix -al2iV17al2iV16apoweraradixainfix -V12c1ainfix -avalue_sub_shiftV0ainfix -V12c1avalue_sub_shiftV1ainfix -V12c1Iainfix <=c0avalue_subapeltsV1aoffsetV1ainfix -ainfix +aoffsetV1V12c1Iainfix al2iV17al2iV16INainfix >ato_intV16ato_intV17Iainfix =avalue_subV32V31ainfix +V30c1ainfix +avalue_subV32V31V30ainfix *al2iagetV32V30apoweraradixainfix -V30V31LapeltsV1LaoffsetV1Lainfix -ainfix +aoffsetV1V12c1Iainfix =avalue_subV29V28ainfix +V27c1ainfix +avalue_subV29V28V27ainfix *al2iagetV29V27apoweraradixainfix -V27V28LapeltsV0LaoffsetV0Lainfix -ainfix +aoffsetV0V12c1Iainfix =acompare_intavalue_sub_shiftV0ap2iV2avalue_sub_shiftV1ap2iV2acompare_intavalue_sub_shiftV0V12avalue_sub_shiftV1V12Iainfix =avalue_subV26V25V23ainfix +avalue_subV26V25V24ainfix *avalue_subV26V24V23apoweraradixainfix -V24V25LapeltsV1LaoffsetV1Lainfix +aoffsetV1V12Lainfix +aoffsetV1ato_intV2Iainfix =avalue_subV22V21V19ainfix +avalue_subV22V21V20ainfix *avalue_subV22V20V19apoweraradixainfix -V20V21LapeltsV0LaoffsetV0Lainfix +aoffsetV0V12Lainfix +aoffsetV0ato_intV2Iainfix =V18aTrueINainfix =ato_intV16ato_intV17Iainfix =V18aTrueAainfix =V18aTrueINainfix =V16V17FIainfix =V17amixfix []acontentsadataV1ainfix +aoffsetV1ato_intV15FIainfix =V16amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV15FIainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V41amixfix []apeltsV1ainfix +aoffsetV1V41Iainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V21amixfix []apeltsV1ainfix +aoffsetV1V21Iainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V22amixfix []apeltsV1ainfix +aoffsetV1V22Iainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V21amixfix []apeltsV1ainfix +aoffsetV1V21Iainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V12amixfix []apeltsV1ainfix +aoffsetV1V12Iainfix =ato_intV5ato_intV6Iainfix =ato_intV6c1FIainfix =amixfix []apeltsV0ainfix +aoffsetV0V12amixfix []apeltsV1ainfix +aoffsetV1V12Iainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FAain_boundsc1Iainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FAainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV1ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV1ap2iV1Aainfix <=c0ap2iV1Iainfix =ato_intV2c0FAain_boundsc0Iavalid_ptr_itvV0ap2iV1F +ad60ff58618a4cc9179cb8b1c2999189 VC for is_zeroiainfix =avalue_sub_shiftV0ap2iV1c0qainfix =ato_intV5c1Aainfix <=ato_intV5c1Aainfix <=c0ato_intV5Iainfix =ato_intV5c1FAain_boundsc1iainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FAain_boundsc1Iainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FAainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV1ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV1ap2iV1Aainfix <=c0ap2iV1Iainfix =ato_intV2c0FAain_boundsc0Iavalid_ptr_itvV0ap2iV1F 8165a33f7d709afc6e795fa9bc6671e9 integer overflowain_boundsc0Iavalid_ptr_itvV0ap2iV1F ece28b26bf664f1b65f7e53695df0edc loop invariant initainfix <=ap2iV1ap2iV1Aainfix <=c0ap2iV1Iainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F 86d9abaa7bf49633e942a8e6b3f65379 loop invariant initainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV1ainfix +aoffsetV0ap2iV1c0Iainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F @@ -108,8 +114,11 @@ b9d8df98e9348e26ab7349e8fd057cdd assertionainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F 1ae9bcca5a5297cc9689f8f2187e09eb preconditionainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F 4e678f0e3c74bc6cb81d74b27e2a2d13 integer overflowain_boundsc0Iainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F -b58d1c4b678cec2a603b143b006dd9fe postconditionainfix <=ato_intV18c1Aainfix <=c0ato_intV18Iainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F -997383c9edb4463a1ca9ebd9fb625f51 postconditionainfix =avalue_sub_shiftV0ap2iV1c0qainfix =ato_intV18c1Iainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F +7d4f4bf3cefa79804b0e250ff247ebdb loop invariant preservationainfix <=ap2iV8ap2iV1Aainfix <=c0ap2iV8IfIainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F +5d35fe099d9591a72627242bc41a448a loop invariant preservationainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV8ainfix +aoffsetV0ap2iV1c0IfIainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F +b8236cdea1f42985345fae7af9622d8f loop variant decreaseainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F +c3796d9755d9479a4b4b40bc2dfce5a1 postconditionainfix <=ato_intV19c1Aainfix <=c0ato_intV19Iainfix =V18V19FIainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F +c684ae73d897343a7c6d1a0b15272826 postconditionainfix =avalue_sub_shiftV0ap2iV1c0qainfix =ato_intV19c1Iainfix =V18V19FIainfix =ato_intV18c0FIainfix <=c0avalue_subapeltsV0ainfix +aoffsetV0V5ainfix +aoffsetV0ato_intV1Iainfix <=ainfix *apoweraradixainfix -ainfix -V15V16c1al2iagetV17ainfix -V15c1avalue_subV17V16V15LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Iainfix =avalue_subV14V13V11ainfix +avalue_subV14V13V12ainfix *avalue_subV14V12V11apoweraradixainfix -V12V13LapeltsV0LaoffsetV0Lainfix +aoffsetV0V5Lainfix +aoffsetV0ato_intV1Iainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F 00a4c212c0cafc66df5c397d3fb1e2ae assertionainfix =ainfix +c1c2c3INainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F 4a7c429d8e2628e2a0ffbf3275905f65 loop invariant preservationainfix <=ap2iV8ap2iV1Aainfix <=c0ap2iV8Iainfix =ainfix +c1c2c3INainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F a524eb6c0d94e3e5f158c573a4f67795 loop invariant preservationainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV8ainfix +aoffsetV0ap2iV1c0Iainfix =ainfix +c1c2c3INainfix =V10aTrueINainfix =ato_intV9ato_intV2Iainfix =V10aTrueAainfix =V10aTrueINainfix =V9V2FIainfix =V9amixfix []acontentsadataV0ainfix +aoffsetV0ato_intV8FIainfix =ato_intV3ato_intV4Iainfix =ato_intV4c1FIainfix =avalue_subapeltsV0ainfix +aoffsetV0ap2iV3ainfix +aoffsetV0ap2iV1c0Aainfix <=ap2iV3ap2iV1Aainfix <=c0ap2iV3FIainfix =ato_intV2c0FIavalid_ptr_itvV0ap2iV1F @@ -1239,11 +1248,15 @@ ce4d148ace55bfbcf7fa26d1b24767f1 assertionainfix =ato_intV20ato_intV2Iainfix =ainfix +ainfix *al2iV18al2iV2al2iV20ainfix +al2iV1ainfix *aradixal2iV0Iainfix =V16c0INainfix >ato_intV20ato_intV10Iainfix =ainfix +ainfix *al2iV18al2iV2V16V7Aainfix =al2iV18V15Iainfix al2iV20al2iV10Iainfix =V16c0Iainfix =al2iV2adivaradixc2F 67f10a81fa43ccec26dfbce6e2b1a735 postconditionainfix =ainfix +ainfix *al2iV18al2iV2al2iV20ainfix +al2iV1ainfix *aradixal2iV0Iainfix =ainfix +ainfix *al2iV18al2iV2al2iV20ainfix +al2iV1ainfix *aradixal2iV0Iainfix =ato_intV20ato_intV2Iainfix =ainfix +ainfix *al2iV18al2iV2al2iV20ainfix +al2iV1ainfix *aradixal2iV0Iainfix =V16c0INainfix >ato_intV20ato_intV10Iainfix =ainfix +ainfix *al2iV18al2iV2V16V7Aainfix =al2iV18V15Iainfix al2iV20al2iV10Iainfix =V16c0Iainfix =al2iV2adivaradixc2F f67145ce89f992dddc3d3e5ebfb0b351 postconditionainfix =ato_intV20ato_intV2Iainfix =ainfix +ainfix *al2iV18al2iV2al2iV20ainfix +al2iV1ainfix *aradixal2iV0Iainfix =V16c0INainfix >ato_intV20ato_intV10Iainfix =ainfix +ainfix *al2iV18al2iV2V16V7Aainfix =al2iV18V15Iainfix al2iV20al2iV10Iainfix =V16c0Iainfix =al2iV2adivaradixc2F -0fa0f3e179db8b06686d792748c9e1c7 VC for from_limbiainfix =avalue_sub_shiftV2c1al2iV0Oais_nullV2Aainfix =aplengthV2c1Oais_nullV2ainfix =avalue_sub_shiftV3c1al2iV0Oais_nullV3Aainfix =aplengthV3c1Oais_nullV3Iainfix =apeltsV3asetapeltsV2aoffsetV3V0Iainfix =alengthacontentsadataV3alengthacontentsadataV2Aainfix =V3amk ptradataV3aoffsetV2FAainfix Int32.to_int sz -> p = old p } + (** break/return*) + + exception Break + + val break () : unit + raises { Break } + returns { _ -> false } + + exception Return32 int32 + + val return32 (x:int32) : unit + raises { Return32 n -> x = n } + returns { _ -> false } + + (** Printing *) + + val print_space () : unit + val print_newline () : unit + + val print_uint32 (n:uint32):unit end diff --git a/src/mlw/cprinter.ml b/src/mlw/cprinter.ml index cf51109b3..334e9476a 100644 --- a/src/mlw/cprinter.ml +++ b/src/mlw/cprinter.ml @@ -41,7 +41,9 @@ module C = struct | Eindex of expr * expr (* Array access *) | Edot of expr * ident (* Field access with dot *) | Earrow of expr * ident (* Pointer access with arrow *) - | Esyntax of string * ty * (ty array) * (expr*ty) list + | Esyntax of string * ty * (ty array) * (expr*ty) list * bool + (* template, type and type arguments of result, typed arguments, + is/is not converter*) and constant = | Cint of string @@ -75,8 +77,9 @@ module C = struct (* [assignify id] transforms a statement that computes a value into a statement that assigns that value to id *) - let rec assignify id = function - | Snop -> raise NotAValue + let rec assignify id s = + match s with + | Snop -> (*Format.printf "assign snop@."; Snop*) raise NotAValue (* ? *) | Sexpr e -> Sexpr (Ebinop (Bassign, Evar id, e)) | Sblock (ds, s) -> Sblock (ds, assignify id s) | Sseq (s1, s2) -> Sseq (s1, assignify id s2) @@ -101,8 +104,8 @@ module C = struct propagate_in_expr id v e2) | Edot (e,i) -> Edot (propagate_in_expr id v e, i) | Earrow (e,i) -> Earrow (propagate_in_expr id v e, i) - | Esyntax (s,t,ta,l) -> - Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l) + | Esyntax (s,t,ta,l,b) -> + Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l,b) | Enothing -> Enothing | Econst c -> Econst c | Esize_type ty -> Esize_type ty @@ -154,6 +157,19 @@ module C = struct let is_empty_block s = s = Sblock([], Snop) let block_of_expr e = [], Sexpr e + + let rec is_nop = function + | Snop -> true + | Sblock ([], s) -> is_nop s + | Sseq (s1,s2) -> is_nop s1 && is_nop s2 + | _ -> false + + let one_stmt = function + | Snop -> true + | Sexpr _ -> true + | Sblock _ -> true + | _ -> false + end type info = Pdriver.printer_args = private { @@ -165,6 +181,147 @@ type info = Pdriver.printer_args = private { converter : Printer.syntax_map; } +module Print = struct + + open C + open Format + open Printer + open Pp + + exception Unprinted of string + + let c_keywords = ["auto"; "break"; "case"; "char"; "const"; "continue"; "default"; "do"; "double"; "else"; "enum"; "extern"; "float"; "for"; "goto"; "if"; "int"; "long"; "register"; "return"; "short"; "signed"; "sizeof"; "static"; "struct"; "switch"; "typedef"; "union"; "unsigned"; "void"; "volatile"; "while" ] + + let () = assert (List.length c_keywords = 32) + + let sanitizer = sanitizer char_to_lalpha char_to_alnumus + let printer = create_ident_printer c_keywords ~sanitizer + + let print_ident fmt id = fprintf fmt "%s" (id_unique printer id) + + let protect_on x s = if x then "(" ^^ s ^^ ")" else s + + let rec print_ty ?(paren=false) fmt = function + | Tvoid -> fprintf fmt "void" + | Tsyntax (s, tl) -> + syntax_arguments + (if paren then ("("^s^")") else s) + (print_ty ~paren:false) fmt tl + | Tptr ty -> fprintf fmt "(%a)*" (print_ty ~paren:true) ty + | Tarray (ty, expr) -> + fprintf fmt (protect_on paren "%a[%a]") + (print_ty ~paren:true) ty (print_expr ~paren:false) expr + | Tstruct _ -> raise (Unprinted "structs") + | Tunion _ -> raise (Unprinted "unions") + | Tnamed id -> print_ident fmt id + | Tnosyntax -> raise (Unprinted "type without syntax") + + and print_unop fmt = function + | Unot -> fprintf fmt "!" + | Ustar -> fprintf fmt "*" + | Uaddr -> fprintf fmt "&" + + and print_binop fmt = function + | Band -> fprintf fmt "&&" + | Bor -> fprintf fmt "||" + | Beq -> fprintf fmt "==" + | Bne -> fprintf fmt "!=" + | Bassign -> fprintf fmt "=" + + and print_expr ~paren fmt = function + | Enothing -> Format.printf "enothing"; () + | Eunop(u,e) -> fprintf fmt (protect_on paren "%a %a") + print_unop u (print_expr ~paren:true) e + | Ebinop(b,e1,e2) -> + fprintf fmt (protect_on paren "%a %a %a") + (print_expr ~paren:true) e1 print_binop b (print_expr ~paren:true) e2 + | Ecast(ty, e) -> + fprintf fmt (protect_on paren "(%a)%a") + (print_ty ~paren:false) ty (print_expr ~paren:true) e + | Ecall (e,l) -> fprintf fmt (protect_on paren "%a(%a)") + (print_expr ~paren:true) e (print_list comma (print_expr ~paren:false)) l + | Econst c -> print_const fmt c + | Evar id -> print_ident fmt id + | Esize_expr e -> + fprintf fmt (protect_on paren "sizeof(%a)") (print_expr ~paren:false) e + | Esize_type ty -> + fprintf fmt (protect_on paren "sizeof(%a)") (print_ty ~paren:false) ty + | Eindex _ | Edot _ | Earrow _ -> raise (Unprinted "struct/array access") + | Esyntax (s, t, args, lte,_) -> + gen_syntax_arguments_typed snd (fun _ -> args) + (if paren then ("("^s^")") else s) + (fun fmt (e,_t) -> print_expr ~paren:false fmt e) + (print_ty ~paren:false) (C.Enothing,t) fmt lte + + and print_const fmt = function + | Cint s | Cfloat s | Cchar s | Cstring s -> fprintf fmt "%s" s + + let print_id_init fmt = function + | id, Enothing -> print_ident fmt id + | id,e -> fprintf fmt "%a = %a" print_ident id (print_expr ~paren:false) e + + let rec print_stmt ~braces fmt = function + | Snop -> Format.printf "snop"; () + | Sexpr e -> fprintf fmt "%a;" (print_expr ~paren:false) e; + | Sblock ([] ,s) when (not braces || one_stmt s) -> (print_stmt ~braces:false) fmt s + | Sblock b -> fprintf fmt "@[{@\n @[%a@]@\n}@]" print_body b + | Sseq (s1,s2) -> fprintf fmt "%a@\n%a" + (print_stmt ~braces:false) s1 + (print_stmt ~braces:false) s2 + | Sif(c,t,e) when is_empty_block e -> + fprintf fmt "if(%a)@\n%a" (print_expr ~paren:false) c + (print_stmt ~braces:true) t + | Sif (c,t,e) -> fprintf fmt "if(%a)@\n%a@\nelse@\n%a" + (print_expr ~paren:false) c + (print_stmt ~braces:true) t + (print_stmt ~braces:true) e + | Swhile (e,b) -> fprintf fmt "while (%a)@ %a" + (print_expr ~paren:false) e (print_stmt ~braces:true) b + | Sfor _ -> raise (Unprinted "for loops") + | Sbreak -> fprintf fmt "break;" + | Sreturn e -> fprintf fmt "return %a;" (print_expr ~paren:true) e + + and print_def fmt = function + | Dfun (id,(rt,args),body) -> + fprintf fmt "%a %a(@[%a@])@ @[{@;<1 2>@[%a@]@\n}@\n@]" + (print_ty ~paren:false) rt + print_ident id + (print_list comma + (print_pair_delim nothing space nothing + (print_ty ~paren:false) print_ident)) + args + print_body body + | Dproto (id, (rt, args)) -> + fprintf fmt "%a %a(@[%a@]);@;" + (print_ty ~paren:false) rt + print_ident id + (print_list comma + (print_pair_delim nothing space nothing + (print_ty ~paren:false) print_ident)) + args + | Ddecl (ty, lie) -> + fprintf fmt "%a @[%a@];@;" + (print_ty ~paren:false) ty + (print_list comma print_id_init) lie + | Dinclude id -> + fprintf fmt "#include<%a.h>@;" print_ident id + | Dtypedef (ty,id) -> + fprintf fmt "@[typedef@ %a@;%a;@]@;" + (print_ty ~paren:false) ty print_ident id + + and print_body fmt body = + print_pair_delim nothing newline nothing + (print_list newline print_def) + (print_stmt ~braces:true) + fmt body + + let print_file fmt info ast = + Mid.iter (fun _ sl -> List.iter (fprintf fmt "%s\n") sl) info.thprelude; + newline fmt (); + fprintf fmt "@[%a@]@." (print_list newline print_def) ast + +end + module Translate = struct open Pdecl open Ity @@ -214,17 +371,21 @@ module Translate = struct let params = List.map (fun pv -> (C.Evar(pv_name pv), ty_of_ty info (ty_of_ity pv.pv_ity))) pvsl in - let rty = ty_of_ity rs.rs_cty.cty_result in + let rty = ty_of_ity e.e_ity in let rtyargs = match rty.ty_node with | Tyvar _ -> [||] | Tyapp (_,args) -> Array.of_list (List.map (ty_of_ty info) args) in - C.Esyntax(s,ty_of_ty info rty, rtyargs, params) + C.Esyntax(s,ty_of_ty info rty, rtyargs, params, + Mid.mem rs.rs_name info.converter) | None -> let args = List.filter (fun pv -> not pv.pv_ghost) pvsl in C.(Ecall(Evar(rs.rs_name), List.map (fun pv -> Evar(pv_name pv)) args)) in - C.([], if is_return then Sreturn e else Sexpr e) + C.([], + if is_return && not (ity_equal rs.rs_cty.cty_result ity_unit) + then Sreturn e + else Sexpr e) | _ -> raise (Unsupported "Cpur/Cany") (*TODO clarify*) end | Eassign _ -> raise (Unsupported "mutable field assign") @@ -233,23 +394,36 @@ module Translate = struct | LDvar (pv,le) -> Format.printf "let %s@." pv.pv_vs.vs_name.id_string; if pv.pv_ghost then expr info ~is_return e - else if ((pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit) + else if ity_equal pv.pv_ity ity_unit then ([], C.Sseq (C.Sblock(expr info ~is_return:false le), C.Sblock(expr info ~is_return e))) else begin match le.e_node with | Econst (Number.ConstInt ic) -> let n = Number.compute_int ic in - let cexp = C.(Econst (Cint (BigInt.to_string n))) in + let ce = C.(Econst (Cint (BigInt.to_string n))) in Format.printf "propagate constant %s for var %s@." (BigInt.to_string n) (pv_name pv).id_string; - C.propagate_in_block (pv_name pv) cexp (expr info ~is_return e) + C.propagate_in_block (pv_name pv) ce (expr info ~is_return e) + | Eexec ({c_node = Capp(rs,_); _},_) + when Mid.mem rs.rs_name info.converter -> + begin match expr info ~is_return:false le with + | [], C.Sexpr(se) -> + C.propagate_in_block (pv_name pv) se (expr info ~is_return e) + | _ -> assert false + end | _-> let t = ty_of_ty info (ty_of_ity pv.pv_ity) in - let d,s = expr info ~is_return:false le in - let initblock = d, C.assignify (pv_name pv) s in - [ C.Ddecl (t, [pv_name pv, C.Enothing]) ], - C.Sseq (C.Sblock initblock, C.Sblock (expr info ~is_return e)) + match expr info ~is_return:false le with + | [], C.Sexpr((C.Esyntax(_,_,_,_,b) as se)) + when b (* converter *) -> + Format.printf "propagate converter for var %s@." + (pv_name pv).id_string; + C.propagate_in_block (pv_name pv) se (expr info ~is_return e) + | d,s -> + let initblock = d, C.assignify (pv_name pv) s in + [ C.Ddecl (t, [pv_name pv, C.Enothing]) ], + C.Sseq (C.Sblock initblock, C.Sblock (expr info ~is_return e)) end | _ -> assert false end @@ -321,10 +495,9 @@ module Translate = struct | _ -> [] (*TODO exn ? *) - let munit info = function | Udecl pd -> pdecl info pd - | Uuse m -> [C.Dinclude m.mod_theory.Theory.th_name] + | Uuse _m -> (*[C.Dinclude m.mod_theory.Theory.th_name]*) [] | Uclone _ -> raise (Unsupported "clone") | Umeta _ -> raise (Unsupported "meta") | Uscope _ -> [] @@ -339,135 +512,7 @@ module Translate = struct end (*TODO simplifications : propagate constants, collapse blocks with only a statement and no def*) -module Print = struct - - open C - open Format - open Printer - open Pp - - exception Unprinted of string - - let c_keywords = ["auto"; "break"; "case"; "char"; "const"; "continue"; "default"; "do"; "double"; "else"; "enum"; "extern"; "float"; "for"; "goto"; "if"; "int"; "long"; "register"; "return"; "short"; "signed"; "sizeof"; "static"; "struct"; "switch"; "typedef"; "union"; "unsigned"; "void"; "volatile"; "while" ] - - let () = assert (List.length c_keywords = 32) - - let sanitizer = sanitizer char_to_lalpha char_to_alnumus - let printer = create_ident_printer c_keywords ~sanitizer - - let print_ident fmt id = fprintf fmt "%s" (id_unique printer id) - - let protect_on x s = if x then "(" ^^ s ^^ ")" else s - - let rec print_ty ?(paren=false) fmt = function - | Tvoid -> fprintf fmt "void" - | Tsyntax (s, tl) -> syntax_arguments s (print_ty ~paren:false) fmt tl - | Tptr ty -> fprintf fmt "(%a)*" (print_ty ~paren:true) ty - | Tarray (ty, expr) -> - fprintf fmt (protect_on paren "%a[%a]") - (print_ty ~paren:true) ty (print_expr ~paren:false) expr - | Tstruct _ -> raise (Unprinted "structs") - | Tunion _ -> raise (Unprinted "unions") - | Tnamed id -> print_ident fmt id - | Tnosyntax -> raise (Unprinted "type without syntax") - - and print_unop fmt = function - | Unot -> fprintf fmt "!" - | Ustar -> fprintf fmt "*" - | Uaddr -> fprintf fmt "&" - - and print_binop fmt = function - | Band -> fprintf fmt "&&" - | Bor -> fprintf fmt "||" - | Beq -> fprintf fmt "==" - | Bne -> fprintf fmt "!=" - | Bassign -> fprintf fmt "=" - - and print_expr ?(paren=false) fmt = function - | Enothing -> Format.printf "enothing"; () - | Eunop(u,e) -> fprintf fmt (protect_on paren "%a %a") - print_unop u (print_expr ~paren:true) e - | Ebinop(b,e1,e2) -> - fprintf fmt (protect_on paren "%a %a %a") - (print_expr ~paren:true) e1 print_binop b (print_expr ~paren:true) e2 - | Ecast(ty, e) -> - fprintf fmt (protect_on paren "(%a)%a") - (print_ty ~paren:false) ty (print_expr ~paren:true) e - | Ecall (e,l) -> fprintf fmt (protect_on paren "%a(%a)") - (print_expr ~paren:true) e (print_list comma (print_expr ~paren:false)) l - | Econst c -> print_const fmt c - | Evar id -> print_ident fmt id - | Esize_expr e -> - fprintf fmt (protect_on paren "sizeof(%a)") (print_expr ~paren:false) e - | Esize_type ty -> - fprintf fmt (protect_on paren "sizeof(%a)") (print_ty ~paren:false) ty - | Eindex _ | Edot _ | Earrow _ -> raise (Unprinted "struct/array access") - | Esyntax (s, t, args, lte) -> - gen_syntax_arguments_typed snd (fun _ -> args) - (if paren then ("("^s^")") else s) - (fun fmt (e,_t) -> print_expr ~paren:false fmt e) - (print_ty ~paren:false) (C.Enothing,t) fmt lte - - and print_const fmt = function - | Cint s | Cfloat s | Cchar s | Cstring s -> fprintf fmt "%s" s - - let print_id_init fmt = function - | id, Enothing -> print_ident fmt id - | id,e -> fprintf fmt "%a = %a" print_ident id (print_expr ~paren:false) e - - let rec print_stmt fmt = function - | Snop -> Format.printf "snop"; () - | Sexpr e -> fprintf fmt "%a;" (print_expr ~paren:false) e; - | Sblock b -> fprintf fmt "@[{@;<1 2>@[%a@]@\n}@]" print_body b - | Sseq (s1,s2) -> fprintf fmt "%a@\n%a" print_stmt s1 print_stmt s2 - | Sif(c,t,e) when is_empty_block e -> - fprintf fmt "if(%a)@\n%a" (print_expr ~paren:false) c print_stmt t - | Sif (c,t,e) -> fprintf fmt "if(%a)@\n%a@\nelse@\n%a" - (print_expr ~paren:false) c print_stmt t print_stmt e - | Swhile (e,b) -> fprintf fmt "while (%a)@ %a" - (print_expr ~paren:false) e print_stmt b - | Sfor _ -> raise (Unprinted "for loops") - | Sbreak -> fprintf fmt "break;" - | Sreturn e -> fprintf fmt "return %a;" (print_expr ~paren:true) e - and print_def fmt = function - | Dfun (id,(rt,args),body) -> - fprintf fmt "%a %a(@[%a@])@ @[{@;<1 2>@[%a@]@;}@;@]" - (print_ty ~paren:false) rt - print_ident id - (print_list comma - (print_pair_delim nothing space nothing - (print_ty ~paren:false) print_ident)) - args - print_body body - | Dproto (id, (rt, args)) -> - fprintf fmt "%a %a(@[%a@]);@;" - (print_ty ~paren:false) rt - print_ident id - (print_list comma - (print_pair_delim nothing space nothing - (print_ty ~paren:false) print_ident)) - args - | Ddecl (ty, lie) -> - fprintf fmt "%a @[%a@];@;" - (print_ty ~paren:false) ty - (print_list comma print_id_init) lie - | Dinclude id -> - fprintf fmt "#include<%a>@;" print_ident id - | Dtypedef (ty,id) -> - fprintf fmt "@[typedef@ %a@;%a;@]@;" - (print_ty ~paren:false) ty print_ident id - - and print_body fmt body = - print_pair_delim nothing newline nothing - (print_list newline print_def) - print_stmt - fmt body - - let print_file fmt = fprintf fmt "@[%a@]@." (print_list newline print_def) - - -end let fg ?fname m = let n = m.Pmodule.mod_theory.Theory.th_name.Ident.id_string in @@ -478,7 +523,7 @@ let fg ?fname m = let pr args ?old fmt m = ignore(old); let ast = Translate.translate args m in - try Print.print_file fmt ast + try Print.print_file fmt args ast with Print.Unprinted s -> (Format.printf "Could not print: %s@." s; Format.fprintf fmt "/* Dummy file */@.") -- GitLab