From 185f016303d7fbdb06fe4380dfcafb08a1beb212 Mon Sep 17 00:00:00 2001 From: Granahir2 Date: Sat, 8 Jun 2024 10:48:13 +0200 Subject: [PATCH] Improved congruence, implemented RP, fixed whitespace. --- analyzer.ml | 6 ++++-- domains/congruence.ml | 6 ++++-- domains/interval.ml | 2 +- domains/naked.ml | 2 +- domains/reduced_product.ml | 5 +++-- domains/value_domain.ml | 2 +- examples/congruence/congruence.c | 5 +++++ examples/congruence/congruence_mul.c | 6 ++++++ iterator/iterator.ml | 32 ++++++++++++++++++++++++++++ 9 files changed, 57 insertions(+), 9 deletions(-) create mode 100644 examples/congruence/congruence.c create mode 100644 examples/congruence/congruence_mul.c diff --git a/analyzer.ml b/analyzer.ml index 8d4d8f7..18b6ad9 100644 --- a/analyzer.ml +++ b/analyzer.ml @@ -19,9 +19,11 @@ let doit filename = begin Cfg_printer.output_dot !Options.cfg_out cfg; let f = match !Options.domain with | "signs" -> SignIterator.iterate cfg - | "interval" -> IntervalIterator.iterate cfg + | "interval" -> IntervalIterator.iterate cfg | "constants" -> ConstIterator.iterate cfg - | _ -> ConstIterator.iterate cfg in + | "congruence" -> CongIterator.iterate cfg + | "product" -> RPIterator.iterate cfg + | _ -> failwith "No valid iterator specified" in Format.printf "@[Failed asserts :@ %a@]" pp_asserts f end diff --git a/domains/congruence.ml b/domains/congruence.ml index ffb7188..638e585 100644 --- a/domains/congruence.ml +++ b/domains/congruence.ml @@ -1,7 +1,7 @@ open Naked open Abstract_syntax_tree -module Congruence : NAKED_VALUE_DOMAIN = struct +module Congruence (*: NAKED_VALUE_DOMAIN*) = struct type t = { multiple : Z.t; offset : Z.t } let all_numbers = { multiple = Z.one; offset = Z.zero } @@ -83,7 +83,9 @@ module Congruence : NAKED_VALUE_DOMAIN = struct offset = Z.div z1.offset z2.offset; } else all_numbers - | AST_MODULO -> all_numbers + | AST_MODULO -> if (Z.equal z2.multiple Z.zero) && (Z.divisible z1.multiple z2.offset) then + const (Z.rem z1.offset z2.offset) + else all_numbers let compatible z = function AST_EQUAL -> z | _ -> raise NeedTop diff --git a/domains/interval.ml b/domains/interval.ml index 1064e6b..6d1c13f 100644 --- a/domains/interval.ml +++ b/domains/interval.ml @@ -1,7 +1,7 @@ open Naked open Abstract_syntax_tree -module Interval : NAKED_VALUE_DOMAIN = struct +module Interval (*: NAKED_VALUE_DOMAIN*) = struct type t = { lower : Z.t; upper : Z.t } let const a = { lower = a; upper = a } diff --git a/domains/naked.ml b/domains/naked.ml index b9229f6..93469a9 100644 --- a/domains/naked.ml +++ b/domains/naked.ml @@ -32,7 +32,7 @@ sig val print: Format.formatter -> t -> unit end -module AddTopBot (N : NAKED_VALUE_DOMAIN) : VALUE_DOMAIN = +module AddTopBot (N : NAKED_VALUE_DOMAIN) (*: VALUE_DOMAIN*) = struct type t = Bot | Top | V of N.t diff --git a/domains/reduced_product.ml b/domains/reduced_product.ml index 842de5d..0dbaf2f 100644 --- a/domains/reduced_product.ml +++ b/domains/reduced_product.ml @@ -35,7 +35,7 @@ module ReducedProduct (C : CROSS_REDUCTION) : VALUE_DOMAIN = struct (C.V.meet (fst p) (fst p')), (C.W.meet (snd p) (snd p'))) - (* we do NOTC.cross-reduce p : it would not guarantee convergence anymore *) + (* we do NOT cross-reduce p : it would not guarantee convergence anymore *) let widen p p' = let p' = C.cr p' in C.V.widen (fst p) (fst p'), C.W.widen (snd p) (snd p') let narrow p p' = let p' = C.cr p' in C.V.narrow (fst p) (fst p'), C.W.narrow (snd p) (snd p') @@ -43,5 +43,6 @@ module ReducedProduct (C : CROSS_REDUCTION) : VALUE_DOMAIN = struct C.V.subset (fst p) (fst p') && C.W.subset (snd p) (snd p') let is_bottom p = (C.cr p) = bottom let print fmt p = - Format.fprintf fmt "@[(%a, %a)@]@ " C.V.print (fst p) C.W.print (snd p) + Format.fprintf fmt "@[(%a, %a)@]" C.V.print (fst p) C.W.print (snd p) end + diff --git a/domains/value_domain.ml b/domains/value_domain.ml index d68edcb..9958fc8 100644 --- a/domains/value_domain.ml +++ b/domains/value_domain.ml @@ -105,7 +105,7 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct let print out env = match env with | Bot -> Format.fprintf out "@[Bot@]" | E map -> begin Format.fprintf out "@[{"; - VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a @ " Cfg_printer.print_var varid V.print val1) map; + VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a@ " Cfg_printer.print_var varid V.print val1) map; Format.fprintf out "}@]"; end let rec compute e expr = match expr with diff --git a/examples/congruence/congruence.c b/examples/congruence/congruence.c new file mode 100644 index 0000000..08d26c6 --- /dev/null +++ b/examples/congruence/congruence.c @@ -0,0 +1,5 @@ +void main() { + int x = rand(0, 10); + x = 2 * x; + assert(x % 2 == 0); +} diff --git a/examples/congruence/congruence_mul.c b/examples/congruence/congruence_mul.c new file mode 100644 index 0000000..3817241 --- /dev/null +++ b/examples/congruence/congruence_mul.c @@ -0,0 +1,6 @@ +void main() { + int x = rand(-4,8); + x = 2*x; + x = 3*x + 2; + assert(x % 6 == 2); +} diff --git a/iterator/iterator.ml b/iterator/iterator.ml index 6a0eb2c..381fe69 100644 --- a/iterator/iterator.ml +++ b/iterator/iterator.ml @@ -93,9 +93,41 @@ open Sign open Constant open Naked open Value_domain +open Congruence +open Reduced_product + +module IntervalxCongr : CROSS_REDUCTION = struct + module V = AddTopBot(Interval) + module W = AddTopBot(Congruence) + let cr (v,w) = match v,w with + | _, W.Bot | V.Bot, _ -> V.Bot, W.Bot + | V.Top, _ | _, W.Top -> v,w + | V.V i, W.V c -> match c.multiple with + | m when Z.equal Z.zero m -> if Z.leq i.lower c.offset && Z.leq c.offset i.upper then + V.V {lower=c.offset; upper=c.offset}, w + else + V.Bot, W.Bot + | m -> (* Non-trivial multiplier : can only hope refining the bounds *) + let q = Z.div (Z.sub i.upper c.offset) m in (*rounds towards zero*) + let q' = Z.div (Z.sub i.lower c.offset) m in + if Z.equal q' q then + let z = Z.add c.offset (Z.mul q' m) in + let newint = V.const z and + newmod = W.const z in newint, newmod + else (if Z.leq q' q then + let newint = V.rand (Z.add c.offset (Z.mul q' m)) + (Z.add c.offset (Z.mul q m)) in + newint, w + else + V.Bot, W.Bot) + +end + module ConstIterator = Iterator(NonRelational(AddTopBot(Constants))) module SignIterator = Iterator(NonRelational(AddTopBot(Signs))) module IntervalIterator = Iterator(NonRelational(AddTopBot(Interval))) +module CongIterator = Iterator(NonRelational(AddTopBot(Congruence))) +module RPIterator = Iterator(NonRelational(ReducedProduct(IntervalxCongr))) (* let iterate cfg = let () = Random.self_init () in