Skip to content

Commit d9b60a8

Browse files
samuelchassotsamuelchassot
authored
Prove invertibility of more functions in ACN (#7)
* unfold the loop in uint2int for verification, proves invertibility of some functions in ACN * invertibility * script to verify acn used functions * remove useless comments * refactor
1 parent 203b54f commit d9b60a8

File tree

4 files changed

+112
-3
lines changed

4 files changed

+112
-3
lines changed

‎asn1scala/src/main/scala/asn1scala/asn1jvm.scala‎

Lines changed: 30 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -302,7 +302,7 @@ def alignedSizeToDWord(bits: Long, offset: Long): Long = {
302302
alignedSizeToN(32L, offset, bits)
303303
}.ensuring(res => bits <= res && res <= bits + 31L)
304304

305-
def uint2int(v: ULong, uintSizeInBytes: Int): Long = {
305+
def uint2intWhile(v: ULong, uintSizeInBytes: Int): Long = {
306306
require(uintSizeInBytes >= 1 && uintSizeInBytes <= 9)
307307

308308
var vv = v.toRaw
@@ -312,7 +312,7 @@ def uint2int(v: ULong, uintSizeInBytes: Int): Long = {
312312
if !bIsNegative then
313313
return v
314314

315-
var i: Int = NO_OF_BYTES_IN_JVM_LONG-1
315+
var i: Int = NO_OF_BYTES_IN_JVM_LONG-1 // 7
316316
(while i >= uintSizeInBytes do
317317
decreases(i)
318318
vv |= ber_aux(i)
@@ -321,6 +321,34 @@ def uint2int(v: ULong, uintSizeInBytes: Int): Long = {
321321
-(~vv) - 1
322322
}
323323

324+
/**
325+
* Version of uint2int that unfolds completely the loop, to help verification
326+
*
327+
* @param v
328+
* @param uintSizeInBytes
329+
*/
330+
def uint2int(v: ULong, uintSizeInBytes: Int): Long = {
331+
require(uintSizeInBytes >= 1 && uintSizeInBytes <= 9)
332+
333+
var vv = v.toRaw
334+
val tmp: ULong = 0x80
335+
val bIsNegative: Boolean = (vv & (tmp << ((uintSizeInBytes - 1) * 8))) > 0
336+
337+
if !bIsNegative then
338+
return v
339+
340+
if(uintSizeInBytes <= 7) then vv |= ber_aux(7)
341+
if(uintSizeInBytes <= 6) then vv |= ber_aux(6)
342+
if(uintSizeInBytes <= 5) then vv |= ber_aux(5)
343+
if(uintSizeInBytes <= 4) then vv |= ber_aux(4)
344+
if(uintSizeInBytes <= 3) then vv |= ber_aux(3)
345+
if(uintSizeInBytes <= 2) then vv |= ber_aux(2)
346+
if(uintSizeInBytes <= 1) then vv |= ber_aux(1)
347+
348+
-(~vv) - 1
349+
}
350+
351+
324352

325353
def GetCharIndex(ch: UByte, charSet: Array[UByte]): Int =
326354
{

‎asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,16 @@ case class ACN(base: Codec) {
223223
require(nBits <= encodedSizeInBits && encodedSizeInBits <= 64)
224224
require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, encodedSizeInBits))
225225
enc_Int_PositiveInteger_ConstSize(intVal.toLong.toRawULong, encodedSizeInBits)
226+
}.ensuring { _ =>
227+
val w1 = old(this)
228+
val w3 = this
229+
w1.base.bitStream.buf.length == w3.base.bitStream.buf.length && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + encodedSizeInBits
230+
&& w1.isPrefixOf(w3) && {
231+
val (r1, r3) = ACN.reader(w1, w3)
232+
validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, encodedSizeInBits)
233+
val (r3Got, iGot) = r1.dec_Int_PositiveInteger_ConstSize_pure(encodedSizeInBits)
234+
iGot.toRaw.toInt == intVal && r3Got == r3
235+
}
226236
}
227237

228238
// @opaque @inlineOnce
@@ -762,23 +772,63 @@ case class ACN(base: Codec) {
762772
require(BitStream.validate_offset_byte(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit))
763773
require(-128L <= intVal && intVal <= 127L)
764774
enc_Int_PositiveInteger_ConstSize_8(ULong.fromRaw(intVal & 0xFFL))
775+
}.ensuring { _ =>
776+
val w1 = old(this)
777+
val w3 = this
778+
w1.base.bufLength() == w3.base.bufLength() && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 8
779+
&& w1.isPrefixOf(w3) && {
780+
val (r1, r3) = ACN.reader(w1, w3)
781+
validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 8)
782+
val (r3Got, iGot) = r1.dec_Int_TwosComplement_ConstSize_8_pure()
783+
iGot == intVal && r3Got == r3
784+
}
765785
}
766786

767787
def enc_Int_TwosComplement_ConstSize_big_endian_16(intVal: Long): Unit = {
768788
require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 16))
769789
require(-32768L <= intVal && intVal <= 32767L)
770790
enc_Int_PositiveInteger_ConstSize_big_endian_16(ULong.fromRaw(intVal & 0xFFFFL))
791+
}.ensuring { _ =>
792+
val w1 = old(this)
793+
val w3 = this
794+
w1.base.bufLength() == w3.base.bufLength() && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 16
795+
&& w1.isPrefixOf(w3) && {
796+
val (r1, r3) = ACN.reader(w1, w3)
797+
validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 16)
798+
val (r3Got, iGot) = r1.dec_Int_TwosComplement_ConstSize_big_endian_16_pure()
799+
iGot == intVal && r3Got == r3
800+
}
771801
}
772802

773803
def enc_Int_TwosComplement_ConstSize_big_endian_32(intVal: Long): Unit = {
774804
require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 32))
775805
require(-2147483648L <= intVal && intVal <= 2147483647L)
776806
enc_Int_PositiveInteger_ConstSize_big_endian_32(ULong.fromRaw(intVal & 0xFFFFFFFFL))
807+
}.ensuring { _ =>
808+
val w1 = old(this)
809+
val w3 = this
810+
w1.base.bufLength() == w3.base.bufLength() && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 32
811+
&& w1.isPrefixOf(w3) && {
812+
val (r1, r3) = ACN.reader(w1, w3)
813+
validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 32)
814+
val (r3Got, iGot) = r1.dec_Int_TwosComplement_ConstSize_big_endian_32_pure()
815+
iGot == intVal && r3Got == r3
816+
}
777817
}
778818

779819
def enc_Int_TwosComplement_ConstSize_big_endian_64(intVal: Long): Unit = {
780820
require(BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 64))
781821
enc_Int_PositiveInteger_ConstSize_big_endian_64(ULong.fromRaw(intVal))
822+
}.ensuring { _ =>
823+
val w1 = old(this)
824+
val w3 = this
825+
w1.base.bufLength() == w3.base.bufLength() && BitStream.bitIndex(w3.base.bitStream.buf.length, w3.base.bitStream.currentByte, w3.base.bitStream.currentBit) == BitStream.bitIndex(w1.base.bitStream.buf.length, w1.base.bitStream.currentByte, w1.base.bitStream.currentBit) + 64
826+
&& w1.isPrefixOf(w3) && {
827+
val (r1, r3) = ACN.reader(w1, w3)
828+
validateOffsetBitsContentIrrelevancyLemma(w1.base.bitStream, w3.base.bitStream.buf, 64)
829+
val (r3Got, iGot) = r1.dec_Int_TwosComplement_ConstSize_big_endian_64_pure()
830+
iGot == intVal && r3Got == r3
831+
}
782832
}
783833

784834
def enc_Int_TwosComplement_ConstSize_little_endian_16(intVal: Long): Unit = {
@@ -832,6 +882,13 @@ case class ACN(base: Codec) {
832882
(cpy, l)
833883
}
834884

885+
@ghost @pure
886+
def dec_Int_TwosComplement_ConstSize_8_pure(): (ACN, Long) = {
887+
888+
val cpy = snapshot(this)
889+
val l = cpy.dec_Int_TwosComplement_ConstSize_8()
890+
(cpy, l)
891+
}
835892

836893
def dec_Int_TwosComplement_ConstSize_8(): Long = {
837894
if(!BitStream.validate_offset_byte(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit) ) then
@@ -840,12 +897,28 @@ case class ACN(base: Codec) {
840897
uint2int(dec_Int_PositiveInteger_ConstSize_8(), 1)
841898
}
842899

900+
@ghost @pure
901+
def dec_Int_TwosComplement_ConstSize_big_endian_16_pure(): (ACN, Long) = {
902+
903+
val cpy = snapshot(this)
904+
val l = cpy.dec_Int_TwosComplement_ConstSize_big_endian_16()
905+
(cpy, l)
906+
}
907+
843908
def dec_Int_TwosComplement_ConstSize_big_endian_16(): Long = {
844909
if(!BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 16) ) then
845910
0L
846911
else
847912
uint2int(dec_Int_PositiveInteger_ConstSize_big_endian_16(), NO_OF_BYTES_IN_JVM_SHORT)
848913
}
914+
915+
@ghost @pure
916+
def dec_Int_TwosComplement_ConstSize_big_endian_32_pure(): (ACN, Long) = {
917+
918+
val cpy = snapshot(this)
919+
val l = cpy.dec_Int_TwosComplement_ConstSize_big_endian_32()
920+
(cpy, l)
921+
}
849922

850923
def dec_Int_TwosComplement_ConstSize_big_endian_32(): Long = {
851924
if(!BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 32)) then
@@ -854,6 +927,14 @@ case class ACN(base: Codec) {
854927
uint2int(dec_Int_PositiveInteger_ConstSize_big_endian_32(), NO_OF_BYTES_IN_JVM_INT)
855928
}
856929

930+
@ghost @pure
931+
def dec_Int_TwosComplement_ConstSize_big_endian_64_pure(): (ACN, Long) = {
932+
933+
val cpy = snapshot(this)
934+
val l = cpy.dec_Int_TwosComplement_ConstSize_big_endian_64()
935+
(cpy, l)
936+
}
937+
857938
def dec_Int_TwosComplement_ConstSize_big_endian_64(): Long = {
858939
if(!BitStream.validate_offset_bits(base.bitStream.buf.length, base.bitStream.currentByte, base.bitStream.currentBit, 64)) then
859940
0L

‎asn1scala/stainless.conf‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
vc-cache = true
55
# debug = ["smt"]
6-
timeout = 120
6+
timeout = 200
77
check-models = false
88
print-ids = false
99
print-types = false

asn1scala/verify_safety_acn.sh renamed to asn1scala/verify_acn_used_fcts.sh

File renamed without changes.

0 commit comments

Comments
 (0)