SMT2 formal verification of security-critical code paths
Git protocol version is determined by enum {protocol_v0=0, protocol_v1=1, protocol_v2=2}. Extracted from discover_version() in connect.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun version () Int)
(assert
(<= version 2))
(assert
(>= version 0))
(assert
(or (< version 0) (> version 2)))
(check-sat)
Protocol negotiation must resolve to an explicitly defined enum value, not just a numerically in-range value.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun version () Int)
(assert
(let (($x29 (= version 2)))
(let (($x28 (= version 1)))
(let (($x27 (= version 0)))
(or $x27 $x28 $x29)))))
(assert
(let (($x29 (= version 2)))
(let (($x28 (= version 1)))
(let (($x27 (= version 0)))
(let (($x26 (or $x27 $x28 $x29)))
(not $x26))))))
(check-sat)
pkt-line protocol limits packets to LARGE_PACKET_MAX (65520). Extracted from packet_read() in pkt-line.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pkt_len () Int)
(assert
(<= pkt_len 65520))
(assert
(>= pkt_len 0))
(assert
(or (< pkt_len 0) (> pkt_len 65520)))
(check-sat)
pkt-line control framing reserves short lengths for 0000/0001/0002 only; 0003 is malformed and must be rejected.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pkt_len () Int)
(assert
(let (($x17 (= pkt_len 2)))
(let (($x5 (= pkt_len 1)))
(let (($x15 (= pkt_len 0)))
(or $x15 $x5 $x17)))))
(assert
(let (($x17 (= pkt_len 2)))
(let (($x5 (= pkt_len 1)))
(let (($x15 (= pkt_len 0)))
(let (($x35 (or $x15 $x5 $x17)))
(and (< pkt_len 4) (not $x35)))))))
(check-sat)
Digest byte widths map to 32-bit word counts: SHA-1=20 bytes (5 words), SHA-256=32 bytes (8 words).
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x5 (= hash_rawsz 32)))
(let (($x26 (= hash_rawsz 20)))
(or $x26 $x5))))
(assert
(or (and (distinct (mod hash_rawsz 4) 0) true) (< (div hash_rawsz 4) 5) (> (div hash_rawsz 4) 8)))
(check-sat)
Hash digest size must be exactly 20 (SHA-1) or 32 (SHA-256). From hash_algos[] compile-time initialization.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x33 (= hash_rawsz 32)))
(let (($x28 (= hash_rawsz 20)))
(or $x28 $x33))))
(assert
(let (($x33 (= hash_rawsz 32)))
(let (($x28 (= hash_rawsz 20)))
(let (($x39 (or $x28 $x33)))
(not $x39)))))
(check-sat)
Tree traversal depth bounded to prevent stack exhaustion. From read_tree_at() recursion.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun tree_depth () Int)
(assert
(<= tree_depth 4096))
(assert
(>= tree_depth 0))
(assert
(or (< tree_depth 0) (> tree_depth 4096)))
(check-sat)
Pathname length bounded by verify_path() in read-cache.c. OS PATH_MAX typically 4096.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun path_len () Int)
(assert
(<= path_len 4096))
(assert
(>= path_len 1))
(assert
(or (< path_len 1) (> path_len 4096)))
(check-sat)
Object types range from OBJ_COMMIT=1 to OBJ_REF_DELTA=7. Defined in object.h enum.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun obj_type () Int)
(assert
(<= obj_type 7))
(assert
(>= obj_type 1))
(assert
(or (< obj_type 1) (> obj_type 7)))
(check-sat)
Object type must be one of the defined types. Type 5 is reserved/invalid.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun obj_type () Int)
(assert
(let (($x15 (= obj_type 7)))
(let (($x11 (= obj_type 6)))
(let (($x14 (= obj_type 4)))
(let (($x13 (= obj_type 3)))
(let (($x28 (= obj_type 2)))
(let (($x16 (= obj_type 1)))
(or $x16 $x28 $x13 $x14 $x11 $x15))))))))
(assert
(let (($x15 (= obj_type 7)))
(let (($x11 (= obj_type 6)))
(let (($x14 (= obj_type 4)))
(let (($x13 (= obj_type 3)))
(let (($x28 (= obj_type 2)))
(let (($x16 (= obj_type 1)))
(let (($x35 (or $x16 $x28 $x13 $x14 $x11 $x15)))
(not $x35)))))))))
(check-sat)
Symbolic ref resolution limited to SYMREF_MAXDEPTH=5 to prevent infinite loops. From refs.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun symref_depth () Int)
(assert
(<= symref_depth 5))
(assert
(>= symref_depth 0))
(assert
(or (< symref_depth 0) (> symref_depth 5)))
(check-sat)
Hash algorithm ID: GIT_HASH_SHA1=1, GIT_HASH_SHA256=2. From repository.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_algo () Int)
(assert
(<= hash_algo 2))
(assert
(>= hash_algo 1))
(assert
(or (< hash_algo 1) (> hash_algo 2)))
(check-sat)
Hash algorithm must be one of the explicitly defined enum members (1 or 2).
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_algo () Int)
(assert
(let (($x14 (= hash_algo 2)))
(let (($x11 (= hash_algo 1)))
(or $x11 $x14))))
(assert
(let (($x14 (= hash_algo 2)))
(let (($x11 (= hash_algo 1)))
(let (($x13 (or $x11 $x14)))
(not $x13)))))
(check-sat)
SHA-1 must use rawsz=20, SHA-256 must use rawsz=32. Enforced by hash_algos[] array.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(declare-fun hash_algo () Int)
(assert
(or (and (= hash_algo 1) (= hash_rawsz 20)) (and (= hash_algo 2) (= hash_rawsz 32))))
(assert
(let (($x7 (or (and (= hash_algo 1) (= hash_rawsz 20)) (and (= hash_algo 2) (= hash_rawsz 32)))))
(not $x7)))
(check-sat)
Digest bit-length must match selected algorithm: SHA-1=160 bits, SHA-256=256 bits.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(declare-fun hash_algo () Int)
(assert
(or (and (= hash_algo 1) (= hash_rawsz 20)) (and (= hash_algo 2) (= hash_rawsz 32))))
(assert
(let (($x66 (or (and (= hash_algo 1) (= (* hash_rawsz 8) 160)) (and (= hash_algo 2) (= (* hash_rawsz 8) 256)))))
(not $x66)))
(check-sat)
Selected hash algorithm must produce canonical object ID hex width: SHA-1=40 chars, SHA-256=64 chars.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(declare-fun hash_algo () Int)
(assert
(or (and (= hash_algo 1) (= hash_rawsz 20)) (and (= hash_algo 2) (= hash_rawsz 32))))
(assert
(let (($x37 (or (and (= hash_algo 1) (= (* hash_rawsz 2) 40)) (and (= hash_algo 2) (= (* hash_rawsz 2) 64)))))
(not $x37)))
(check-sat)
Pack object header is 1-MAX_PACK_OBJECT_HEADER(10) bytes. From encode_in_pack_object_header() in pack-write.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun header_len () Int)
(assert
(<= header_len 10))
(assert
(>= header_len 1))
(assert
(or (< header_len 1) (> header_len 10)))
(check-sat)
Hash raw size ranges from 20 (SHA-1) to 32 (SHA-256).
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x57 (= hash_rawsz 32)))
(let (($x61 (= hash_rawsz 20)))
(or $x61 $x57))))
(assert
(or (< hash_rawsz 20) (> hash_rawsz 32)))
(check-sat)
Hash digest bit-length: SHA-1=160, SHA-256=256.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x66 (= hash_rawsz 32)))
(let (($x41 (= hash_rawsz 20)))
(or $x41 $x66))))
(assert
(or (< (* hash_rawsz 8) 160) (> (* hash_rawsz 8) 256)))
(check-sat)
Hash digest bit-length must map exactly to supported algorithms: SHA-1=160, SHA-256=256.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x49 (= hash_rawsz 32)))
(let (($x52 (= hash_rawsz 20)))
(or $x52 $x49))))
(assert
(let (($x14 (or (= (* hash_rawsz 8) 160) (= (* hash_rawsz 8) 256))))
(not $x14)))
(check-sat)
Hash raw size must be 4-byte aligned: 20 and 32 are both word-aligned.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x20 (= hash_rawsz 32)))
(let (($x12 (= hash_rawsz 20)))
(or $x12 $x20))))
(assert
(let ((?x57 (mod hash_rawsz 4)))
(and (distinct ?x57 0) true)))
(check-sat)
Hex object IDs must be exactly 40 chars (SHA-1) or 64 chars (SHA-256), derived from hash raw size.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x12 (= hash_rawsz 32)))
(let (($x37 (= hash_rawsz 20)))
(or $x37 $x12))))
(assert
(let (($x60 (or (= (* hash_rawsz 2) 40) (= (* hash_rawsz 2) 64))))
(not $x60)))
(check-sat)
Hash raw size must be an even number of bytes to avoid half-byte (nibble) truncation during hex object ID handling.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun hash_rawsz () Int)
(assert
(let (($x56 (= hash_rawsz 32)))
(let (($x45 (= hash_rawsz 20)))
(or $x45 $x56))))
(assert
(let ((?x36 (mod hash_rawsz 2)))
(and (distinct ?x36 0) true)))
(check-sat)