[cost] Fix the model of substring

Summary:
This diff fixes the model of substring.

Problem: The cost model of the substring function was to return `size of string - start index` as a
cost.  However, sometimes this was a negative number, because of state abstractions on paths, array
elements, call contexts, etc, which caused an exception inadvertently.

This diff changes the model to return just `size of string`, when it cannot say `size of string` is
bigger than `start index`.

Reviewed By: ezgicicek

Differential Revision: D18707954

fbshipit-source-id: 63f27e461
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent fb56f42716
commit 8fa098474e

@ -49,8 +49,11 @@ end
module JavaString = struct
let substring_aux ~begin_idx ~end_v {integer_type_widths; location} inferbo_mem =
let begin_v = BufferOverrunSemantics.eval integer_type_widths begin_idx inferbo_mem in
let begin_itv = BufferOverrunDomain.Val.get_itv begin_v in
let end_itv = BufferOverrunDomain.Val.get_itv end_v in
let itv =
Itv.minus (BufferOverrunDomain.Val.get_itv end_v) (BufferOverrunDomain.Val.get_itv begin_v)
if Boolean.is_true (Itv.le_sem begin_itv end_itv) then Itv.minus end_itv begin_itv
else end_itv
in
CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.substring"
location

@ -29,4 +29,9 @@ class StringTest {
int index = indexof_linear(mId);
return mId.substring(0, index);
}
private String startsWith_constant() {
String s = "";
return s.startsWith(",") ? s.substring(1) : s;
}
}

Loading…
Cancel
Save