diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index fa220552f1..f1169c40fc 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -440,8 +440,10 @@ struct if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then ( let unify_st' = match r with | Some lv -> - assign_to_global_wrapper (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg unify_st lv (fun st v -> - RD.assign_var st.rel (RV.local v) RV.return + let ask = Analyses.ask_of_ctx ctx in + assign_to_global_wrapper ask ctx.global ctx.sideg unify_st lv (fun st v -> + let rel = RD.assign_var st.rel (RV.local v) RV.return in + assert_type_bounds ask rel v (* TODO: should be done in return instead *) ) | None -> unify_st diff --git a/src/autoTune.ml b/src/autoTune.ml index e4b03acf84..b1c834cd5a 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -335,20 +335,22 @@ let isComparison = function let isGoblintStub v = List.exists (fun (Attr(s,_)) -> s = "goblint_stub") v.vattr let rec extractVar = function - | UnOp (Neg, e, _) -> extractVar e - | Lval ((Var info),_) when not (isGoblintStub info) -> Some info + | UnOp (Neg, e, _) + | CastE (_, e) -> extractVar e + | Lval ((Var info),_) when not (isGoblintStub info) -> Some info | _ -> None +let extractBinOpVars e1 e2 = + match extractVar e1, extractVar e2 with + | Some a, Some b -> [a; b] + | Some a, None when isConstant e2 -> [a] + | None, Some b when isConstant e1 -> [b] + | _, _ -> [] + let extractOctagonVars = function | BinOp (PlusA, e1,e2, (TInt _)) - | BinOp (MinusA, e1,e2, (TInt _)) -> ( - match extractVar e1, extractVar e2 with - | Some a, Some b -> Some (`Left (a,b)) - | Some a, None - | None, Some a -> if isConstant e1 then Some (`Right a) else None - | _,_ -> None - ) - | _ -> None + | BinOp (MinusA, e1,e2, (TInt _)) -> extractBinOpVars e1 e2 + | e -> Option.to_list (extractVar e) let addOrCreateVarMapping varMap key v globals = if key.vglob = globals then varMap := if VariableMap.mem key !varMap then @@ -357,25 +359,19 @@ let addOrCreateVarMapping varMap key v globals = if key.vglob = globals then var else VariableMap.add key v !varMap -let handle varMap v globals = function - | Some (`Left (a,b)) -> - addOrCreateVarMapping varMap a v globals; - addOrCreateVarMapping varMap b v globals; - | Some (`Right a) -> addOrCreateVarMapping varMap a v globals; - | None -> () - class octagonVariableVisitor(varMap, globals) = object inherit nopCilVisitor method! vexpr = function (*an expression of type +/- a +/- b where a,b are either variables or constants*) | BinOp (op, e1,e2, (TInt _)) when isComparison op -> ( - handle varMap 5 globals (extractOctagonVars e1) ; - handle varMap 5 globals (extractOctagonVars e2) ; + List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e1); + List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e2); DoChildren ) - | Lval ((Var info),_) when not (isGoblintStub info) -> handle varMap 1 globals (Some (`Right info)) ; SkipChildren + | Lval ((Var info),_) when not (isGoblintStub info) -> addOrCreateVarMapping varMap info 1 globals; SkipChildren (*Traverse down only operations fitting for linear equations*) + | UnOp (LNot, _,_) | UnOp (Neg, _,_) | BinOp (PlusA,_,_,_) | BinOp (MinusA,_,_,_) diff --git a/tests/regression/29-svcomp/35-nla-sqrt.c b/tests/regression/29-svcomp/35-nla-sqrt.c new file mode 100644 index 0000000000..dc382181cc --- /dev/null +++ b/tests/regression/29-svcomp/35-nla-sqrt.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --enable ana.sv-comp.functions --enable ana.autotune.enabled --set ana.autotune.activated[+] octagon +// Extracted from: nla-digbench-scaling/sqrt1-ll_unwindbound5.c +#include +extern int __VERIFIER_nondet_int(void); + +int main() { + int n; + long long s; + n = __VERIFIER_nondet_int(); + + if (!(s <= n)) { + __goblint_check(s > n); + } else { + __goblint_check(s <= 2147483647); + } + + return 0; +} diff --git a/tests/regression/29-svcomp/dune b/tests/regression/29-svcomp/dune index 23c0dd3290..2aede4e50b 100644 --- a/tests/regression/29-svcomp/dune +++ b/tests/regression/29-svcomp/dune @@ -1,2 +1,16 @@ +(rule + (aliases runtest runaprontest) + (enabled_if %{lib-available:apron}) + (deps + (package goblint) + ../../../goblint ; update_suite calls local goblint + (:update_suite ../../../scripts/update_suite.rb) + (glob_files ??-*.c)) + (locks /update_suite) + (action + (chdir ../../.. + (progn + (run %{update_suite} nla-sqrt -q))))) + (cram (deps (glob_files *.c)))