search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
443 stars 93 forks source link

VST upgrade 2.6 -> 2.8: 80% slowdown in compilation time #514

Open zoickx opened 3 years ago

zoickx commented 3 years ago

Related: [vst-user] mailing list thread, VST performance thread on Coq discoruse.

After upgrading our relatively large (43KLOC) C verification project from VST version 2.6 to 2.8 (along with ocaml and some others), we've encountered a major increase in compilation time: from 3.2 to 5.7 hours on single thread.

Following are the benchmarks of the same project before and after VST upgrade (with only minor fixes made).

VST 2.6

Opam switch Using [coq-config](https://github.com/vzaliva/coq-config). **NOTE**: despite it being included in the base compiler, Coq was built without [flambda support](https://coq.discourse.group/t/install-notes-on-ocaml-versions-and-coq-configuration/713). ``` yaml opam: switch: asn1 compiler: 4.11.2+flambda repositories: - name: coq-released address: https://coq.inria.fr/opam/released dependencies: - coq.8.12.2 # mehirlib pinned for compcert compatibility - coq-menhirlib.20210310 - coq-compcert.3.7+8.12~coq_platform - coq-vst.2.6 - coq-ext-lib - name: coq-struct-tact kind: git target: https://github.com/uwplse/StructTact.git ```
Slowest lines Based on `coq_makefile`'s `TIMING=1`. ``` 3647.168s [(forward_call~~~(0,...] ./Lib/BCT/Vst.v 375.093s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 321.073s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 320.115s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 235.524s [entailer~!.] ./Primitive/Int/VstEnc.v 167.235s [entailer~!.] ./Primitive/Int/VstEnc.v 148.394s [entailer~!.] ./Lib/BCT/Vst.v 129.598s [entailer~!.] ./Primitive/Int/VstEnc.v 129.445s [entailer~!.] ./Primitive/Int/VstEnc.v 118.361s [entailer~!.] ./Lib/BCT/Vst.v 100.696s [entailer~!.] ./Primitive/Int/VstEnc.v 96.793s [entailer~!.] ./Primitive/Int/VstEnc.v 89.982s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 89.85s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 89.327s [(repeat~forward).] ./Primitive/Int/VstEnc.v 83.463s [(repeat~forward).] ./Primitive/Int/VstEnc.v 80.93s [all:~~(try~list_sol...] ./Lib/DWT/VST/Der_write_TL.v 77.918s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 74.784s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 74.691s [(repeat~forward).] ./Primitive/Int/VstEnc.v 74.67s [(repeat~forward).] ./Primitive/Int/VstEnc.v 72.069s [Qed.] ./Primitive/Prim/Ber_decode_primitive.v 70.863s [entailer~!.] ./Lib/BCT/Vst.v 69.792s [(repeat~forward).] ./Primitive/Int/VstEnc.v 69.532s [entailer~!.] ./Primitive/Int/VstEnc.v 68.866s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 64.763s [Time~(do~6~forward).] ./Primitive/Int/VstEnc.v 64.644s [(repeat~forward).] ./Primitive/Int/VstEnc.v 64.469s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 64.417s [(repeat~forward).] ./Primitive/Int/VstEnc.v 60.921s [Time~forward_call~~...] ./Lib/DWT/VST/Der_write_TL.v 58.864s [Qed.] ./Lib/DWT/VST/Der_write_tags.v 54.448s [(forward_if_add_sep...] ./Lib/BCT/Vst.v 52.72s [Qed.] ./Primitive/Int/VstEnc.v 52.129s [(repeat~forward).] ./Primitive/Int/VstEnc.v 51.658s [(repeat~forward).] ./Primitive/Int/VstEnc.v 48.788s [all:~~(try~list_sol...] ./Lib/DWT/VST/Der_write_TL.v 46.697s [Qed.] ./Lib/DWT/VST/Der_write_TL.v 45.971s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 44.253s [(forward_if~(temp~_...] ./Lib/BCT/Vst.v 43.473s [Qed.] ./Primitive/Prim/Der_encode_primitive.v 43.429s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 42.058s [Admitted.] ./Lib/BCT/Vst.v 41.616s [(repeat~break_if;~r...] ./Lib/BCT/Vst.v 41.133s [(repeat~forward).] ./Lib/BCT/Vst.v 40.796s [entailer~!.] ./Lib/BCT/Vst.v 39.977s [entailer~!.] ./Primitive/Int/VstEnc.v 39.204s [(repeat~split;~auto...] ./Lib/DWT/VST/Der_write_tags.v 38.578s [entailer~!.] ./Primitive/Int/VstEnc.v 37.398s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v ```
Time+Memory per file Based on `coq_makefile`'s `pretty-timed`. ``` Time | Peak Mem | File Name -------------------------------------------------------------------- 193m24.00s | 15940112 ko | Total Time / Peak Mem -------------------------------------------------------------------- 67m37.29s | 4643276 ko | Primitive/Int/VstEnc.vo 60m15.17s | 15940112 ko | Lib/BCT/Vst.vo 17m22.32s | 3032852 ko | Primitive/Prim/Der_encode_primitive.vo 13m59.24s | 6918888 ko | Primitive/Prim/Ber_decode_primitive.vo 10m42.94s | 3782684 ko | Lib/DWT/VST/Der_write_tags.vo 6m00.66s | 3145416 ko | Lib/DWT/VST/Der_write_TL.vo 5m17.98s | 1462856 ko | Lib/DWT/VST/Ber_tlv_tag_serialize.vo 5m09.90s | 1541464 ko | Lib/DWT/VST/Ber_tlv_length_serialize.vo 1m33.63s | 1382892 ko | Lib/BCT/BFT/Vst.vo 1m25.55s | 793196 ko | Core/SepLemmas.vo 0m50.21s | 761504 ko | Correctness/IntegerCorrectnessCtoESPEC.vo 0m31.64s | 1118868 ko | Lib/Callback/Overrun.vo 0m30.64s | 739732 ko | Lib/DWT/Exec/Der_write_tags_lemmas.vo 0m20.74s | 788996 ko | Correctness/TagCorrectness.vo 0m13.79s | 792832 ko | Lib/BCT/BFL/Vst.vo 0m12.09s | 723444 ko | Correctness/LengthCorrectness.vo 0m10.57s | 721712 ko | Correctness/IntegerCorrectness.vo 0m07.75s | 728960 ko | Lib/BCT/VST/ASN__STACK_OVERFLOW_CHECK.vo 0m07.27s | 713356 ko | Correctness/PrimitiveCorrectness.vo 0m04.94s | 711296 ko | Correctness/Roundtrip.vo 0m04.42s | 713896 ko | Primitive/Int/Exec.vo 0m04.34s | 688120 ko | Lib/BCT/BFT/Exec.vo 0m04.24s | 668328 ko | Lib/DWT/Exec/Der_write_TL_m.vo 0m03.72s | 539508 ko | Core/Lemmas/Int.vo 0m03.62s | 706836 ko | Lib/BCT/Exec.vo 0m03.10s | 679804 ko | Lib/DWT/Exec/Ber_tlv_tag_serialize.vo 0m02.90s | 678044 ko | Lib/DWT/Exec/Ber_tlv_length_serialize.vo 0m01.36s | 517460 ko | Clight/INTEGER.vo 0m01.29s | 652008 ko | Correctness/AbstractSpec.vo 0m01.25s | 678988 ko | Lib/BCT/BFL/Exec.vo 0m01.24s | 661492 ko | Lib/Stdlib.vo 0m01.21s | 676924 ko | Lib/DWT/Exec/Der_write_tags.vo 0m01.21s | 672024 ko | Lib/VstLib.vo 0m01.12s | 654300 ko | Primitive/Prim/Exec.vo 0m01.07s | 509812 ko | Clight/asn_application.vo 0m01.06s | 664924 ko | Core/Tactics.vo 0m01.06s | 665796 ko | Lib/Lib.vo 0m01.03s | 670464 ko | Lib/Forward.vo 0m01.02s | 506208 ko | Clight/BOOLEAN.vo 0m01.01s | 661608 ko | Core/Lemmas/Ptr.vo 0m00.98s | 661104 ko | Core/Lemmas/IntPtr.vo 0m00.98s | 669460 ko | Core/VstTactics.vo 0m00.93s | 505180 ko | Clight/ber_decoder.vo 0m00.92s | 501288 ko | Clight/ber_tlv_tag.vo 0m00.90s | 500708 ko | Clight/der_encoder.vo 0m00.89s | 501260 ko | Clight/ber_tlv_length.vo 0m00.74s | 500672 ko | Clight/asn_codecs_prim.vo 0m00.53s | 513624 ko | Lib/Types.vo 0m00.51s | 495808 ko | Core/Core.vo 0m00.49s | 506128 ko | Core/StructNormalizer.vo 0m00.48s | 507260 ko | Core/Notations.vo 0m00.07s | 83936 ko | Lib/ErrorWithWriter.vo ```

VST 2.8

Opam switch Using [coq-config](https://github.com/vzaliva/coq-config). ``` yaml opam: switch: asn1-vst28 compiler: 4.12.0 repositories: - name: coq-released address: https://coq.inria.fr/opam/released dependencies: - coq-vst-32.2.8 - coq-ext-lib - name: coq-struct-tact kind: git target: https://github.com/uwplse/StructTact.git ```
Slowest lines Based on `coq_makefile`'s `TIMING=1`. ``` 1308.14s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 1166.323s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 1135.149s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 815.389s [(forward_call~(b,~i...] ./Lib/BCT/Vst.v 783.205s [entailer~!.] ./Primitive/Int/VstEnc.v 550.485s [entailer~!.] ./Primitive/Int/VstEnc.v 423.423s [entailer~!.] ./Primitive/Int/VstEnc.v 423.125s [entailer~!.] ./Primitive/Int/VstEnc.v 372.832s [Qed.] ./Lib/BCT/Vst.v 328.5s [entailer~!.] ./Primitive/Int/VstEnc.v 313.906s [entailer~!.] ./Primitive/Int/VstEnc.v 293.308s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 277.73s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 263.443s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 253.546s [Time~forward_call~~...] ./Lib/DWT/VST/Der_write_TL.v 222.464s [entailer~!.] ./Primitive/Int/VstEnc.v 197.869s [(repeat~split;~auto...] ./Lib/DWT/VST/Der_write_tags.v 163.584s [Qed.] ./Primitive/Prim/Ber_decode_primitive.v 145.246s [all:~(try~list_solve).] ./Primitive/Int/VstEnc.v 136.935s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 136.053s [Qed.] ./Primitive/Int/VstEnc.v 135.111s [(repeat~forward).] ./Primitive/Int/VstEnc.v 122.781s [Qed.] ./Lib/DWT/VST/Der_write_tags.v 122.204s [entailer~!.] ./Primitive/Int/VstEnc.v 120.961s [Qed.] ./Lib/DWT/VST/Der_write_TL.v 119.822s [entailer~!.] ./Primitive/Int/VstEnc.v 119.217s [(repeat~forward).] ./Primitive/Int/VstEnc.v 119.215s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 116.29s [(repeat~forward).] ./Primitive/Int/VstEnc.v 116.109s [(repeat~forward).] ./Primitive/Int/VstEnc.v 115.486s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 112.608s [all:~~(try~list_sol...] ./Lib/DWT/VST/Der_write_TL.v 111.057s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 109.684s [entailer~!.] ./Primitive/Int/VstEnc.v 103.02s [(repeat~forward).] ./Primitive/Int/VstEnc.v 100.408s [(destruct~l;~try~li...] ./Primitive/Prim/Der_encode_primitive.v 98.715s [(repeat~forward).] ./Primitive/Prim/Der_encode_primitive.v 94.236s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 93.545s [forward_call~~(fi,~...] ./Lib/DWT/VST/Der_write_tags.v 89.622s [forward_call~~(Int....] ./Lib/DWT/VST/Der_write_tags.v 88.402s [(repeat~forward).] ./Primitive/Int/VstEnc.v 87.875s [(repeat~forward).] ./Primitive/Int/VstEnc.v 85.007s [entailer~!.] ./Primitive/Int/VstEnc.v 84.436s [Qed.] ./Primitive/Prim/Der_encode_primitive.v 80.557s [entailer~!.] ./Primitive/Prim/Der_encode_primitive.v 76.962s [Time~(do~6~forward).] ./Primitive/Int/VstEnc.v 75.464s [(repeat~forward).] ./Primitive/Int/VstEnc.v 75.132s [(repeat~forward).] ./Primitive/Int/VstEnc.v 74.369s [all:~~(try~list_sol...] ./Lib/DWT/VST/Der_write_TL.v 68.954s [entailer~!.] ./Primitive/Int/VstEnc.v ```
Time+Memory per file Based on `coq_makefile`'s `pretty-timed`. ``` Time | Peak Mem | File Name -------------------------------------------------------------------- 342m37.29s | 15930984 ko | Total Time / Peak Mem -------------------------------------------------------------------- 180m16.27s | 5848024 ko | Primitive/Int/VstEnc.vo 44m17.31s | 15930984 ko | Lib/BCT/Vst.vo 40m28.68s | 4617116 ko | Primitive/Prim/Der_encode_primitive.vo 25m03.57s | 7345444 ko | Primitive/Prim/Ber_decode_primitive.vo 20m18.79s | 6111724 ko | Lib/DWT/VST/Der_write_tags.vo 12m09.03s | 7469188 ko | Lib/DWT/VST/Der_write_TL.vo 5m56.43s | 1469284 ko | Lib/DWT/VST/Ber_tlv_tag_serialize.vo 5m42.19s | 1513680 ko | Lib/DWT/VST/Ber_tlv_length_serialize.vo 2m08.18s | 1604036 ko | Lib/BCT/BFT/Vst.vo 1m29.87s | 745388 ko | Core/SepLemmas.vo 0m51.43s | 718156 ko | Correctness/IntegerCorrectnessCtoESPEC.vo 0m44.83s | 1075060 ko | Lib/Callback/Overrun.vo 0m31.97s | 1005408 ko | Lib/BCT/BFL/Vst.vo 0m31.22s | 692524 ko | Lib/DWT/Exec/Der_write_tags_lemmas.vo 0m26.36s | 851804 ko | Lib/BCT/VST/ASN__STACK_OVERFLOW_CHECK.vo 0m20.56s | 737936 ko | Correctness/TagCorrectness.vo 0m11.69s | 682360 ko | Correctness/LengthCorrectness.vo 0m10.07s | 669408 ko | Correctness/IntegerCorrectness.vo 0m07.26s | 662364 ko | Correctness/PrimitiveCorrectness.vo 0m04.52s | 661684 ko | Correctness/Roundtrip.vo 0m04.23s | 641120 ko | Lib/BCT/BFT/Exec.vo 0m03.93s | 648972 ko | Primitive/Int/Exec.vo 0m03.75s | 523280 ko | Core/Lemmas/Int.vo 0m03.72s | 628664 ko | Lib/DWT/Exec/Der_write_TL_m.vo 0m03.26s | 645012 ko | Lib/BCT/Exec.vo 0m02.79s | 629132 ko | Lib/DWT/Exec/Ber_tlv_tag_serialize.vo 0m02.74s | 627816 ko | Lib/DWT/Exec/Ber_tlv_length_serialize.vo 0m01.46s | 514764 ko | Clight/INTEGER.vo 0m01.33s | 507920 ko | Clight/asn_application.vo 0m01.15s | 624856 ko | Correctness/AbstractSpec.vo 0m01.14s | 621320 ko | Lib/Stdlib.vo 0m01.13s | 500268 ko | Clight/ber_tlv_tag.vo 0m01.11s | 503488 ko | Clight/BOOLEAN.vo 0m01.11s | 500332 ko | Clight/ber_tlv_length.vo 0m01.09s | 501880 ko | Clight/ber_decoder.vo 0m01.09s | 498624 ko | Clight/der_encoder.vo 0m00.98s | 627336 ko | Lib/BCT/BFL/Exec.vo 0m00.97s | 632040 ko | Lib/VstLib.vo 0m00.95s | 624420 ko | Core/Tactics.vo 0m00.93s | 623152 ko | Lib/Forward.vo 0m00.92s | 618000 ko | Core/Lemmas/Ptr.vo 0m00.92s | 621864 ko | Lib/Lib.vo 0m00.91s | 626684 ko | Primitive/Prim/Exec.vo 0m00.90s | 628140 ko | Lib/DWT/Exec/Der_write_tags.vo 0m00.89s | 621932 ko | Core/VstTactics.vo 0m00.86s | 484280 ko | Clight/asn_codecs_prim.vo 0m00.83s | 617424 ko | Core/Lemmas/IntPtr.vo 0m00.50s | 482228 ko | Core/StructNormalizer.vo 0m00.48s | 490460 ko | Lib/Types.vo 0m00.47s | 483256 ko | Core/Notations.vo 0m00.46s | 396724 ko | Core/Core.vo 0m00.07s | 67956 ko | Lib/ErrorWithWriter.vo ```

Sure, our code is not well optimzed, but the exact same tactic invocations are taking up to 4 times as long after the upgrade.

Furethermore, peak memory consumption of 15GiB is achieved in the same tactic invocation under both versions. Here are some details:

Peak memory tactic Runninng ``` coq forward_call (0, b, (i + (Ptrofs.repr (Int.signed i0)))%ptrofs, (Int.repr size - i0)%int, sublist (Int.signed i0) (len ptr) ptr, v_tlv_len). ``` for goal corresponding to [this](https://github.com/vlm/asn1c/blob/9925dbbda86b436896108439ea3e0a31280a6065/skeletons/ber_decoder.c#L207) line in C: ``` coq Espec : OracleKind opt_codec_ctx_p, td_p : val td : TYPE_descriptor tags_p : val b : block i : ptrofs ptr : list int res_p : val size : Z last_length_p : val max_stack_size : Z Delta_specs := abbreviate : PTree.t funspec Delta := abbreviate : tycontext v_tlv_tag, v_tlv_len, v_rval, v_rval__1, v_rval__2, v_rval__3, v_rval__4, v_rval__5, v_rval__6, v_rval__7, v_rval__8, v_rval__9, v_rval__10, v_rval__11, v_rval__12 : val i0, i1 : int Heqp : Exec.ber_fetch_tags ptr size = (i0, i1) H : (Znth (Int.signed i0) ptr & Int.repr 128)%int = 0 /\ 0 < len ptr - Int.signed i0 H2 : 0 < len ptr <= Int.max_signed H3 : (Znth 0 ptr & Int.repr 32)%int = 0 H6 : 1 = len (tags td) H7 : 0 <= Ptrofs.unsigned i + len ptr <= Ptrofs.max_unsigned H8 : Forall (fun x : int => 0 <= Int.signed x <= Byte.max_signed) ptr H9 : 0 <= size <= 32 /\ size = len ptr A : -1 <= ASN__STACK_OVERFLOW_CHECK 0 max_stack_size <= 0 H0 : opt_codec_ctx_p <> nullval H1 : ASN__STACK_OVERFLOW_CHECK 0 max_stack_size = 0 i2, i3 : int Heqp0 : Exec.ber_fetch_len (sublist (Int.signed i0) (len ptr) ptr) 0 0 (Int.repr size - i0)%int (Int.repr (sizeof tuint)) (Int.repr Int.max_signed) = (i2, i3) ptr' : list val Heqptr' : ptr' = map Vint ptr POSTCONDITION := abbreviate : ret_assert z : Z Heqb0 : z = 0 H4 : 0 <= z <= 1 H5 : z < len (tags td) LLL : size < Int.max_signed PPP : size = len ptr H10 : ((i0 == Int.repr (-1)) || (i0 == 0))%bool = false H11 : Vptr b i = field_address (tarray tuchar (len ptr)) (SUB 0) (Vptr b i) H12 : i1 = Int.repr (Znth z (tags td)) MORE_COMMANDS := abbreviate : statement G : 0 <= size <= 32 U : size = len ptr B : i0 = fst (i0, i1) -> ((i0 == 0) || (i0 == Int.repr (-1)))%bool = false -> 0 <= Int.signed i0 II : 0 < Int.signed i0 H13 : (Znth (Int.signed i0) ptr & Int.repr 128)%int = 0 H14 : 0 < len ptr - Int.signed i0 D : data_at Tsh (tarray tuchar (len ptr)) (map Vint ptr) (Vptr b i) = (data_at Tsh (tarray tuchar (Int.signed i0)) (map Vint (sublist 0 (Int.signed i0) ptr)) (Vptr b i) * data_at Tsh (tarray tuchar (len (sublist (Int.signed i0) (len ptr) ptr))) (map Vint (sublist (Int.signed i0) (len ptr) ptr)) (Vptr b (i + Ptrofs.repr (Int.signed i0))%ptrofs))%logic ============================ semax Delta (PROP (True) LOCAL (temp _t'35 (Vint (Int.repr (len (tags td)))); temp _t'16 Vzero; temp _tlv_constr (Vint 0); temp _t'14 Vzero; temp _t'39 (Znth 0 (map Vint ptr)); temp _t'13 (if i0 == Int.repr (-1) then Vint 1 else Val.of_bool (i0 == Int.repr 0)); temp _tag_len (Vint i0); temp _t'40 (Vint (Int.repr (len (tags td)))); temp _tagno (Vint (Int.repr z)); temp _step (Vint (Int.repr z)); temp _expect_00_terminators (Vint (Int.repr 0)); temp _limit_len (Vint (Int.repr (-1))); temp _consumed_myself (Vint 0); lvar _rval__12 (Tstruct _asn_dec_rval_s noattr) v_rval__12; lvar _rval__11 (Tstruct _asn_dec_rval_s noattr) v_rval__11; lvar _rval__10 (Tstruct _asn_dec_rval_s noattr) v_rval__10; lvar _rval__9 (Tstruct _asn_dec_rval_s noattr) v_rval__9; lvar _rval__8 (Tstruct _asn_dec_rval_s noattr) v_rval__8; lvar _rval__7 (Tstruct _asn_dec_rval_s noattr) v_rval__7; lvar _rval__6 (Tstruct _asn_dec_rval_s noattr) v_rval__6; lvar _rval__5 (Tstruct _asn_dec_rval_s noattr) v_rval__5; lvar _rval__4 (Tstruct _asn_dec_rval_s noattr) v_rval__4; lvar _rval__3 (Tstruct _asn_dec_rval_s noattr) v_rval__3; lvar _rval__2 (Tstruct _asn_dec_rval_s noattr) v_rval__2; lvar _rval__1 (Tstruct _asn_dec_rval_s noattr) v_rval__1; lvar _rval (Tstruct _asn_dec_rval_s noattr) v_rval; lvar _tlv_len tint v_tlv_len; lvar _tlv_tag tuint v_tlv_tag; temp __res res_p; temp _opt_codec_ctx opt_codec_ctx_p; temp _td td_p; temp _opt_ctx nullval; temp _ptr (Vptr b i); temp _size (Vint (Int.repr size)); temp _tag_mode (Vint (Int.repr 0)); temp _last_tag_form (Vint (Int.repr 0)); temp _last_length last_length_p; temp _opt_tlv_form nullval) SEP (data_at Tsh (tarray tuchar (Int.signed i0)) (map Vint (sublist 0 (Int.signed i0) ptr)) (Vptr b i) * data_at Tsh (tarray tuchar (len (sublist (Int.signed i0) (len ptr) ptr))) (map Vint (sublist (Int.signed i0) (len ptr) ptr)) (Vptr b (i + Ptrofs.repr (Int.signed i0))%ptrofs); if ((i0 == Int.repr (-1)) || (i0 == 0))%bool then data_at_ Tsh tuint v_tlv_tag else data_at Tsh tuint (Vint i1) v_tlv_tag; data_at Tsh (Tstruct _asn_codec_ctx_s noattr) (Vint (Int.repr max_stack_size)) opt_codec_ctx_p; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__12; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__11; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__10; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__9; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__8; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__7; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__6; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__5; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__4; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__3; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__2; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval__1; data_at_ Tsh (Tstruct _asn_dec_rval_s noattr) v_rval; data_at_ Tsh tint v_tlv_len; field_at Tsh (Tstruct _asn_TYPE_descriptor_s noattr) (DOT _tags) tags_p td_p; field_at Tsh (Tstruct _asn_TYPE_descriptor_s noattr) (DOT _tags_count) (Vint (Int.repr (len (tags td)))) td_p; data_at Tsh (tarray tuint (len (tags td))) (map Vint (map Int.repr (tags td))) tags_p; data_at_ Tsh asn_dec_rval_s res_p; data_at_ Tsh tint last_length_p)) ((_t'20 = _ber_fetch_length (_tlv_constr, ((tptr tschar) _ptr + _tag_len), (_size - _tag_len), &_tlv_len); _len_len = _t'20;) MORE_COMMANDS) POSTCONDITION ```
andrew-appel commented 3 years ago

Can you provide more information about the funspec of the function ber_fetch_length ? That might help me in replicating the problem so that I can fix it. For example, I conjectured that the problem was related to the very large number of addressable local variables (corresponding to the many lvar and data_at_ clauses in your current precondition), so on that basis I tried this experiment:

int f(int x) { return x; }
struct foo { int x; };
int g(void) {
  struct foo a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12;
  return f(0);
}

Within g, just at the forward_call to function f, there are then 12 lvars and 12 data_at_ in the precondition. But the forward_call takes just 2.163 seconds on my machine. So that does not seem to be the problem. I have also tried experiments with many temp vars, and experiments with many function parameters for the function f, and I also cannot replicate the slowdown.

(Of course, perhaps it goes fast on my machine because I have a core i7 processor...)

andrew-appel commented 3 years ago

More measurements, shown here demonstrate that having 20 lvars, with the associated 20 data_at conjuncts, and functions with between 0 and 20 pointer parameters (with the corresponding 0 to 20 data_at conjuncts in the precondition), does not lead to exponential slowdown.

So, this issue report illustrates some performance problem in VST, but it's not simply the number of variables, or the number of function parameters, or the number of SEP conjuncts.