Skip to content
GitLab
Commit bcfcfe0e authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following: 

commit b736ae79
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Thu May 2 16:53:39 2019 -0700

    Update README.md.

commit a263f213
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Thu May 2 16:25:07 2019 -0700

    Move benchmarks from pending repository.
parent c35d070b
Expand all Hide whitespace changes
Inline Side-by-side
2019-Gonzalvez/opStructure_C_16_32_2_2.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_MBA_6.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_MBA_7.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_NPT_1.smt2 0 → 100644
View file @ bcfcfe0e
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)
; This file was generated with the help of KLEE
(set-info :source |
Generated by: Alexandre Gonzalvez
Generated on: 2019-02-28
Generator: KLEE
Target solver: Boolector Z3 STP
Benchmarks arising from a generator of opaque expressions
These expressions are used to protect some constants against
reverse-engineering, but their robustness can be compromised by
SMT-solvers
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
; Number of instructions: 475
; Time expected : less than 1 minute
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat (select x (_ bv3 32) ) (concat (select x (_ bv2 32) ) (concat (select x (_ bv1 32) ) (select x (_ bv0 32) ) ) ) ) ) ) (let ( (?B2 (bvmul ?B1 ?B1 ) ) ) (let ( (?B3 (bvmul (_ bv715827882 32) ?B2 ) ) ) (let ( (?B4 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B3 ) (_ bv2 32) ) ) ?B3 ) ) ) (let ( (?B5 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B4 ) (_ bv2 32) ) ) ?B4 ) ) ) (let ( (?B6 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B5 ) (_ bv2 32) ) ) ?B5 ) ) ) (let ( (?B7 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B6 ) (_ bv2 32) ) ) ?B6 ) ) ) (let ( (?B8 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B7 ) (_ bv2 32) ) ) ?B7 ) ) ) (let ( (?B9 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B8 ) (_ bv2 32) ) ) ?B8 ) ) ) (let ( (?B10 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B9 ) (_ bv2 32) ) ) ?B9 ) ) ) (let ( (?B11 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B10 ) (_ bv2 32) ) ) ?B10 ) ) ) (let ( (?B12 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B11 ) (_ bv2 32) ) ) ?B11 ) ) ) (let ( (?B13 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B12 ) (_ bv2 32) ) ) ?B12 ) ) ) (let ( (?B14 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B13 ) (_ bv2 32) ) ) ?B13 ) ) ) (let ( (?B15 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B14 ) (_ bv2 32) ) ) ?B14 ) ) ) (let ( (?B16 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B15 ) (_ bv2 32) ) ) ?B15 ) ) ) (let ( (?B17 (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B16 ) (_ bv2 32) ) ) ?B16 ) ) ) (and (= (_ bv3657258328 32) (bvadd (bvmul ?B2 (bvlshr (bvadd (_ bv2863311530 32) ?B17 ) (_ bv2 32) ) ) ?B17 ) ) (= (_ bv1 32) (concat (select model_version (_ bv3 32) ) (concat (select model_version (_ bv2 32) ) (concat (select model_version (_ bv1 32) ) (select model_version (_ bv0 32) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
(check-sat)
(exit)
2019-Gonzalvez/opStructure_NPT_2.smt2 0 → 100644
View file @ bcfcfe0e
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)
; This file conforms to SMTLIBv2 and was generated by KLEE
(set-info :source |
Generated by: Alexandre Gonzalvez
Generated on: 2019-02-28
Generator: KLEE
Target solver: Boolector Z3 STP
Benchmarks arising from a generator of opaque expressions
These expressions are used to protect some constants against
reverse-engineering, but their robustness can be compromised by
SMT-solvers
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
; Number of instructions: 627
; Time expected : less than 1 minute
; Array declarations
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
; Constraints
; Constraints and QueryExpr
(assert
(let
(
(?B1
(concat
(select
x
(_ bv3 32)
)
(concat
(select
x
(_ bv2 32)
)
(concat
(select
x
(_ bv1 32)
)
(select
x
(_ bv0 32)
)
)
)
)
)
)
(let
(
(?B2
(bvmul
(_ bv715827882 32)
?B1
)
)
)
(let
(
(?B3
(bvadd
?B2
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B2
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B4
(bvadd
?B3
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B3
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B5
(bvadd
?B4
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B4
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B6
(bvadd
?B5
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B5
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B7
(bvadd
?B6
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B6
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B8
(bvadd
?B7
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B7
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B9
(bvadd
?B8
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B8
)
(_ bv2 32)
)
)
)
)
)
(let
(
(?B10
(bvadd
?B9
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B9
)
(_ bv2 32)
)
)
)
)
)
(and
(=
(_ bv1506744832 32)
(bvadd
?B10
(bvmul
?B1
(bvlshr
(bvadd
(_ bv2863311530 32)
?B10
)
(_ bv2 32)
)
)
)
)
(=
(_ bv1 32)
(concat
(select
model_version
(_ bv3 32)
)
(concat
(select
model_version
(_ bv2 32)
)
(concat
(select
model_version
(_ bv1 32)
)
(select
model_version
(_ bv0 32)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(check-sat)
(exit)
2019-Gonzalvez/opStructure_O_16_24_2_2.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_O_16_32_2_2.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_O_32_16_2_2.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Gonzalvez/opStructure_O_32_32_2_2.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/VexRiscv-regch0-15-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/VexRiscv-regch0-20-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/VexRiscv-regch0-30-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/picorv32-check-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/picorv32-pcregs-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/zipcpu-busdelay-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/zipcpu-pfcache-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2018E/zipcpu-zipmmu-compact-mem.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
2019-Wolf-fmbench/2019A/picorv32_mutAX_QF_AUFBV_NONINCR.smt2 0 → 100644
View file @ bcfcfe0e
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment